Proof of Theorem 2exeu
Step | Hyp | Ref
| Expression |
1 | | excom 1551 |
. . . . 5
⊢ (∃y∃xφ ↔ ∃x∃yφ) |
2 | | hbe1 1381 |
. . . . . . . 8
⊢ (∃xφ → ∀x∃xφ) |
3 | 2 | hbmo 1936 |
. . . . . . 7
⊢ (∃*y∃xφ → ∀x∃*y∃xφ) |
4 | 3 | 19.41h 1572 |
. . . . . 6
⊢ (∃x(∃yφ ∧ ∃*y∃xφ) ↔ (∃x∃yφ ∧ ∃*y∃xφ)) |
5 | | 19.8a 1479 |
. . . . . . . . 9
⊢ (φ → ∃xφ) |
6 | 5 | moimi 1962 |
. . . . . . . 8
⊢ (∃*y∃xφ → ∃*yφ) |
7 | 6 | anim2i 324 |
. . . . . . 7
⊢ ((∃yφ ∧ ∃*y∃xφ) → (∃yφ ∧ ∃*yφ)) |
8 | 7 | eximi 1488 |
. . . . . 6
⊢ (∃x(∃yφ ∧ ∃*y∃xφ) → ∃x(∃yφ ∧ ∃*yφ)) |
9 | 4, 8 | sylbir 125 |
. . . . 5
⊢ ((∃x∃yφ ∧ ∃*y∃xφ) → ∃x(∃yφ ∧ ∃*yφ)) |
10 | 1, 9 | sylanb 268 |
. . . 4
⊢ ((∃y∃xφ ∧ ∃*y∃xφ) → ∃x(∃yφ ∧ ∃*yφ)) |
11 | | simpl 102 |
. . . . . 6
⊢ ((∃yφ ∧ ∃*yφ) → ∃yφ) |
12 | 11 | moimi 1962 |
. . . . 5
⊢ (∃*x∃yφ → ∃*x(∃yφ ∧ ∃*yφ)) |
13 | 12 | adantl 262 |
. . . 4
⊢ ((∃x∃yφ ∧ ∃*x∃yφ) → ∃*x(∃yφ ∧ ∃*yφ)) |
14 | 10, 13 | anim12i 321 |
. . 3
⊢ (((∃y∃xφ ∧ ∃*y∃xφ) ∧ (∃x∃yφ ∧ ∃*x∃yφ)) → (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ))) |
15 | 14 | ancoms 255 |
. 2
⊢ (((∃x∃yφ ∧ ∃*x∃yφ) ∧ (∃y∃xφ ∧ ∃*y∃xφ)) → (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ))) |
16 | | eu5 1944 |
. . 3
⊢ (∃!x∃yφ ↔ (∃x∃yφ ∧ ∃*x∃yφ)) |
17 | | eu5 1944 |
. . 3
⊢ (∃!y∃xφ ↔ (∃y∃xφ ∧ ∃*y∃xφ)) |
18 | 16, 17 | anbi12i 433 |
. 2
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ((∃x∃yφ ∧ ∃*x∃yφ) ∧ (∃y∃xφ ∧ ∃*y∃xφ))) |
19 | | eu5 1944 |
. . 3
⊢ (∃!x∃!yφ ↔ (∃x∃!yφ ∧ ∃*x∃!yφ)) |
20 | | eu5 1944 |
. . . . 5
⊢ (∃!yφ ↔ (∃yφ ∧ ∃*yφ)) |
21 | 20 | exbii 1493 |
. . . 4
⊢ (∃x∃!yφ ↔ ∃x(∃yφ ∧ ∃*yφ)) |
22 | 20 | mobii 1934 |
. . . 4
⊢ (∃*x∃!yφ ↔ ∃*x(∃yφ ∧ ∃*yφ)) |
23 | 21, 22 | anbi12i 433 |
. . 3
⊢ ((∃x∃!yφ ∧ ∃*x∃!yφ) ↔ (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ))) |
24 | 19, 23 | bitri 173 |
. 2
⊢ (∃!x∃!yφ ↔ (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ))) |
25 | 15, 18, 24 | 3imtr4i 190 |
1
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) → ∃!x∃!yφ) |