Proof of Theorem 2mo
Step | Hyp | Ref
| Expression |
1 | | 2mo2 2673 |
. . . 4
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
2 | | nfmo1 2566 |
. . . . . . 7
⊢
Ⅎ𝑥∃*𝑥∃𝑦𝜑 |
3 | | nftru 1767 |
. . . . . . . . 9
⊢
Ⅎ𝑦⊤ |
4 | | nfe1 2085 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∃𝑥𝜑 |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ Ⅎ𝑥∃𝑥𝜑) |
6 | 3, 5 | nfmodv 2568 |
. . . . . . . 8
⊢ (⊤
→ Ⅎ𝑥∃*𝑦∃𝑥𝜑) |
7 | 6 | mptru 1514 |
. . . . . . 7
⊢
Ⅎ𝑥∃*𝑦∃𝑥𝜑 |
8 | 2, 7 | nfan 1862 |
. . . . . 6
⊢
Ⅎ𝑥(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) |
9 | | nftru 1767 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⊤ |
10 | | nfe1 2085 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∃𝑦𝜑 |
11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ Ⅎ𝑦∃𝑦𝜑) |
12 | 9, 11 | nfmodv 2568 |
. . . . . . . . 9
⊢ (⊤
→ Ⅎ𝑦∃*𝑥∃𝑦𝜑) |
13 | 12 | mptru 1514 |
. . . . . . . 8
⊢
Ⅎ𝑦∃*𝑥∃𝑦𝜑 |
14 | | nfmo1 2566 |
. . . . . . . 8
⊢
Ⅎ𝑦∃*𝑦∃𝑥𝜑 |
15 | 13, 14 | nfan 1862 |
. . . . . . 7
⊢
Ⅎ𝑦(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) |
16 | | 19.8a 2107 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑦𝜑) |
17 | | spsbe 2031 |
. . . . . . . . . 10
⊢ ([𝑤 / 𝑦]𝜑 → ∃𝑦𝜑) |
18 | 17 | sbimi 2023 |
. . . . . . . . 9
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑧 / 𝑥]∃𝑦𝜑) |
19 | | nfv 1873 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧∃𝑦𝜑 |
20 | 19 | mo3 2573 |
. . . . . . . . . . 11
⊢
(∃*𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧)) |
21 | 20 | biimpi 208 |
. . . . . . . . . 10
⊢
(∃*𝑥∃𝑦𝜑 → ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧)) |
22 | 21 | 19.21bbi 2116 |
. . . . . . . . 9
⊢
(∃*𝑥∃𝑦𝜑 → ((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧)) |
23 | 16, 18, 22 | syl2ani 597 |
. . . . . . . 8
⊢
(∃*𝑥∃𝑦𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑥 = 𝑧)) |
24 | | 19.8a 2107 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑥𝜑) |
25 | | sbcom2 2408 |
. . . . . . . . . 10
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑) |
26 | | spsbe 2031 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑥]𝜑 → ∃𝑥𝜑) |
27 | 26 | sbimi 2023 |
. . . . . . . . . 10
⊢ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑) |
28 | 25, 27 | sylbi 209 |
. . . . . . . . 9
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑) |
29 | | nfv 1873 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑤∃𝑥𝜑 |
30 | 29 | mo3 2573 |
. . . . . . . . . . 11
⊢
(∃*𝑦∃𝑥𝜑 ↔ ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤)) |
31 | 30 | biimpi 208 |
. . . . . . . . . 10
⊢
(∃*𝑦∃𝑥𝜑 → ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤)) |
32 | 31 | 19.21bbi 2116 |
. . . . . . . . 9
⊢
(∃*𝑦∃𝑥𝜑 → ((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤)) |
33 | 24, 28, 32 | syl2ani 597 |
. . . . . . . 8
⊢
(∃*𝑦∃𝑥𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑦 = 𝑤)) |
34 | 23, 33 | anim12ii 608 |
. . . . . . 7
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
35 | 15, 34 | alrimi 2141 |
. . . . . 6
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
36 | 8, 35 | alrimi 2141 |
. . . . 5
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
37 | 36 | alrimivv 1887 |
. . . 4
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
38 | 1, 37 | sylbir 227 |
. . 3
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
39 | | nfs1v 2200 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 |
40 | | nfs1v 2200 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[𝑤 / 𝑦]𝜑 |
41 | 40 | nfsbv 2268 |
. . . . . . . . 9
⊢
Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 |
42 | | pm3.21 464 |
. . . . . . . . . 10
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (𝜑 → (𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))) |
43 | 42 | imim1d 82 |
. . . . . . . . 9
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
44 | 41, 43 | alimd 2140 |
. . . . . . . 8
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
45 | 39, 44 | alimd 2140 |
. . . . . . 7
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
46 | 45 | com12 32 |
. . . . . 6
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
47 | 46 | aleximi 1794 |
. . . . 5
⊢
(∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
48 | 47 | aleximi 1794 |
. . . 4
⊢
(∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
49 | | 2nexaln 1792 |
. . . . . 6
⊢ (¬
∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑) |
50 | | nfv 1873 |
. . . . . . 7
⊢
Ⅎ𝑤𝜑 |
51 | | nfv 1873 |
. . . . . . 7
⊢
Ⅎ𝑧𝜑 |
52 | 50, 51 | 2sb8ev 2286 |
. . . . . 6
⊢
(∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
53 | 49, 52 | xchnxbi 324 |
. . . . 5
⊢ (¬
∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑) |
54 | | pm2.21 121 |
. . . . . . . . 9
⊢ (¬
𝜑 → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
55 | 54 | 2alimi 1775 |
. . . . . . . 8
⊢
(∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
56 | 55 | 2eximi 1798 |
. . . . . . 7
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
57 | 56 | 19.23bi 2117 |
. . . . . 6
⊢
(∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
58 | 57 | 19.23bi 2117 |
. . . . 5
⊢
(∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
59 | 53, 58 | sylbi 209 |
. . . 4
⊢ (¬
∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
60 | 48, 59 | pm2.61d1 173 |
. . 3
⊢
(∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
61 | 38, 60 | impbii 201 |
. 2
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
62 | | alrot4 2095 |
. 2
⊢
(∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
63 | 61, 62 | bitri 267 |
1
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |