Proof of Theorem 2eu6
Step | Hyp | Ref
| Expression |
1 | | 2eu4 2655 |
. 2
⊢
((∃!𝑥∃𝑦𝜑 ∧ ∃!𝑦∃𝑥𝜑) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
2 | | nfia1 2156 |
. . . . . 6
⊢
Ⅎ𝑥(∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
3 | | nfa1 2154 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) |
4 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝑥 = 𝑧 |
5 | | simpl 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧) |
6 | 5 | imim2i 16 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → 𝑥 = 𝑧)) |
7 | 6 | sps 2184 |
. . . . . . . . . . . . 13
⊢
(∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → 𝑥 = 𝑧)) |
8 | 3, 4, 7 | exlimd 2218 |
. . . . . . . . . . . 12
⊢
(∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑦𝜑 → 𝑥 = 𝑧)) |
9 | | ax12v 2178 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (∃𝑦𝜑 → ∀𝑥(𝑥 = 𝑧 → ∃𝑦𝜑))) |
10 | 8, 9 | syli 39 |
. . . . . . . . . . 11
⊢
(∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑦𝜑 → ∀𝑥(𝑥 = 𝑧 → ∃𝑦𝜑))) |
11 | 10 | com12 32 |
. . . . . . . . . 10
⊢
(∃𝑦𝜑 → (∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥(𝑥 = 𝑧 → ∃𝑦𝜑))) |
12 | 11 | spsd 2186 |
. . . . . . . . 9
⊢
(∃𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥(𝑥 = 𝑧 → ∃𝑦𝜑))) |
13 | | nfs1v 2159 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦[𝑤 / 𝑦]𝜑 |
14 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) |
15 | 14 | imim2i 16 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → 𝑦 = 𝑤)) |
16 | | sbequ1 2247 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → (𝜑 → [𝑤 / 𝑦]𝜑)) |
17 | 15, 16 | syli 39 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → [𝑤 / 𝑦]𝜑)) |
18 | 17 | sps 2184 |
. . . . . . . . . . . . 13
⊢
(∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → [𝑤 / 𝑦]𝜑)) |
19 | 3, 13, 18 | exlimd 2218 |
. . . . . . . . . . . 12
⊢
(∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑦𝜑 → [𝑤 / 𝑦]𝜑)) |
20 | 19 | imim2d 57 |
. . . . . . . . . . 11
⊢
(∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ((𝑥 = 𝑧 → ∃𝑦𝜑) → (𝑥 = 𝑧 → [𝑤 / 𝑦]𝜑))) |
21 | 20 | al2imi 1823 |
. . . . . . . . . 10
⊢
(∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∀𝑥(𝑥 = 𝑧 → ∃𝑦𝜑) → ∀𝑥(𝑥 = 𝑧 → [𝑤 / 𝑦]𝜑))) |
22 | | sb6 2093 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑧 → [𝑤 / 𝑦]𝜑)) |
23 | | 2sb6 2094 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) |
24 | 22, 23 | bitr3i 280 |
. . . . . . . . . 10
⊢
(∀𝑥(𝑥 = 𝑧 → [𝑤 / 𝑦]𝜑) ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) |
25 | 21, 24 | syl6ib 254 |
. . . . . . . . 9
⊢
(∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∀𝑥(𝑥 = 𝑧 → ∃𝑦𝜑) → ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))) |
26 | 12, 25 | sylcom 30 |
. . . . . . . 8
⊢
(∃𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))) |
27 | 26 | ancld 554 |
. . . . . . 7
⊢
(∃𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ∧ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)))) |
28 | | 2albiim 1898 |
. . . . . . 7
⊢
(∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ∧ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))) |
29 | 27, 28 | syl6ibr 255 |
. . . . . 6
⊢
(∃𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
30 | 2, 29 | exlimi 2217 |
. . . . 5
⊢
(∃𝑥∃𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
31 | 30 | 2eximdv 1927 |
. . . 4
⊢
(∃𝑥∃𝑦𝜑 → (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
32 | 31 | imp 410 |
. . 3
⊢
((∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
33 | | biimpr 223 |
. . . . . . 7
⊢ ((𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) |
34 | 33 | 2alimi 1820 |
. . . . . 6
⊢
(∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) |
35 | 34 | 2eximi 1843 |
. . . . 5
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) |
36 | | 2exsb 2360 |
. . . . 5
⊢
(∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) |
37 | 35, 36 | sylibr 237 |
. . . 4
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑥∃𝑦𝜑) |
38 | | biimp 218 |
. . . . . 6
⊢ ((𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
39 | 38 | 2alimi 1820 |
. . . . 5
⊢
(∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
40 | 39 | 2eximi 1843 |
. . . 4
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
41 | 37, 40 | jca 515 |
. . 3
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
42 | 32, 41 | impbii 212 |
. 2
⊢
((∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
43 | 1, 42 | bitri 278 |
1
⊢
((∃!𝑥∃𝑦𝜑 ∧ ∃!𝑦∃𝑥𝜑) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |