Proof of Theorem cbvexdh
Step | Hyp | Ref
| Expression |
1 | | ax-17 1416 |
. . 3
⊢ (φ → ∀xφ) |
2 | | ax-17 1416 |
. . . 4
⊢ (χ → ∀xχ) |
3 | 2 | hbex 1524 |
. . 3
⊢ (∃yχ → ∀x∃yχ) |
4 | | cbvexdh.1 |
. . . . 5
⊢ (φ → ∀yφ) |
5 | | cbvexdh.2 |
. . . . 5
⊢ (φ → (ψ → ∀yψ)) |
6 | | cbvexdh.3 |
. . . . . 6
⊢ (φ → (x = y →
(ψ ↔ χ))) |
7 | | equcomi 1589 |
. . . . . . 7
⊢ (y = x →
x = y) |
8 | | bicom1 122 |
. . . . . . 7
⊢ ((ψ ↔ χ) → (χ ↔ ψ)) |
9 | 7, 8 | imim12i 53 |
. . . . . 6
⊢
((x = y → (ψ
↔ χ)) → (y = x →
(χ ↔ ψ))) |
10 | 6, 9 | syl 14 |
. . . . 5
⊢ (φ → (y = x →
(χ ↔ ψ))) |
11 | 4, 5, 10 | equsexd 1614 |
. . . 4
⊢ (φ → (∃y(y = x ∧ χ) ↔
ψ)) |
12 | | simpr 103 |
. . . . 5
⊢
((y = x ∧ χ) → χ) |
13 | 12 | eximi 1488 |
. . . 4
⊢ (∃y(y = x ∧ χ) →
∃yχ) |
14 | 11, 13 | syl6bir 153 |
. . 3
⊢ (φ → (ψ → ∃yχ)) |
15 | 1, 3, 14 | exlimdh 1484 |
. 2
⊢ (φ → (∃xψ → ∃yχ)) |
16 | 1, 5 | eximdh 1499 |
. . . 4
⊢ (φ → (∃xψ → ∃x∀yψ)) |
17 | | 19.12 1552 |
. . . 4
⊢ (∃x∀yψ → ∀y∃xψ) |
18 | 16, 17 | syl6 29 |
. . 3
⊢ (φ → (∃xψ → ∀y∃xψ)) |
19 | 2 | a1i 9 |
. . . . 5
⊢ (φ → (χ → ∀xχ)) |
20 | 1, 19, 6 | equsexd 1614 |
. . . 4
⊢ (φ → (∃x(x = y ∧ ψ) ↔
χ)) |
21 | | simpr 103 |
. . . . 5
⊢
((x = y ∧ ψ) → ψ) |
22 | 21 | eximi 1488 |
. . . 4
⊢ (∃x(x = y ∧ ψ) →
∃xψ) |
23 | 20, 22 | syl6bir 153 |
. . 3
⊢ (φ → (χ → ∃xψ)) |
24 | 4, 18, 23 | exlimd2 1483 |
. 2
⊢ (φ → (∃yχ → ∃xψ)) |
25 | 15, 24 | impbid 120 |
1
⊢ (φ → (∃xψ ↔ ∃yχ)) |