Proof of Theorem 2mo
Step | Hyp | Ref
| Expression |
1 | | 2mo2 2650 |
. . . 4
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
2 | | nfmo1 2558 |
. . . . . . 7
⊢
Ⅎ𝑥∃*𝑥∃𝑦𝜑 |
3 | | nfe1 2153 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑥𝜑 |
4 | 3 | nfmov 2561 |
. . . . . . 7
⊢
Ⅎ𝑥∃*𝑦∃𝑥𝜑 |
5 | 2, 4 | nfan 1907 |
. . . . . 6
⊢
Ⅎ𝑥(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) |
6 | | nfe1 2153 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑦𝜑 |
7 | 6 | nfmov 2561 |
. . . . . . . 8
⊢
Ⅎ𝑦∃*𝑥∃𝑦𝜑 |
8 | | nfmo1 2558 |
. . . . . . . 8
⊢
Ⅎ𝑦∃*𝑦∃𝑥𝜑 |
9 | 7, 8 | nfan 1907 |
. . . . . . 7
⊢
Ⅎ𝑦(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) |
10 | | 19.8a 2180 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑦𝜑) |
11 | | spsbe 2090 |
. . . . . . . . . 10
⊢ ([𝑤 / 𝑦]𝜑 → ∃𝑦𝜑) |
12 | 11 | sbimi 2082 |
. . . . . . . . 9
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑧 / 𝑥]∃𝑦𝜑) |
13 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧∃𝑦𝜑 |
14 | 13 | mo3 2565 |
. . . . . . . . . . 11
⊢
(∃*𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧)) |
15 | 14 | biimpi 219 |
. . . . . . . . . 10
⊢
(∃*𝑥∃𝑦𝜑 → ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧)) |
16 | 15 | 19.21bbi 2189 |
. . . . . . . . 9
⊢
(∃*𝑥∃𝑦𝜑 → ((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧)) |
17 | 10, 12, 16 | syl2ani 610 |
. . . . . . . 8
⊢
(∃*𝑥∃𝑦𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑥 = 𝑧)) |
18 | | 19.8a 2180 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑥𝜑) |
19 | | sbcom2 2167 |
. . . . . . . . . 10
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑) |
20 | | spsbe 2090 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑥]𝜑 → ∃𝑥𝜑) |
21 | 20 | sbimi 2082 |
. . . . . . . . . 10
⊢ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑) |
22 | 19, 21 | sylbi 220 |
. . . . . . . . 9
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑) |
23 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑤∃𝑥𝜑 |
24 | 23 | mo3 2565 |
. . . . . . . . . . 11
⊢
(∃*𝑦∃𝑥𝜑 ↔ ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤)) |
25 | 24 | biimpi 219 |
. . . . . . . . . 10
⊢
(∃*𝑦∃𝑥𝜑 → ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤)) |
26 | 25 | 19.21bbi 2189 |
. . . . . . . . 9
⊢
(∃*𝑦∃𝑥𝜑 → ((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤)) |
27 | 18, 22, 26 | syl2ani 610 |
. . . . . . . 8
⊢
(∃*𝑦∃𝑥𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑦 = 𝑤)) |
28 | 17, 27 | anim12ii 621 |
. . . . . . 7
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
29 | 9, 28 | alrimi 2213 |
. . . . . 6
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
30 | 5, 29 | alrimi 2213 |
. . . . 5
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
31 | 30 | alrimivv 1936 |
. . . 4
⊢
((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
32 | 1, 31 | sylbir 238 |
. . 3
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
33 | | nfs1v 2159 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 |
34 | | nfs1v 2159 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[𝑤 / 𝑦]𝜑 |
35 | 34 | nfsbv 2331 |
. . . . . . . . 9
⊢
Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 |
36 | | pm3.21 475 |
. . . . . . . . . 10
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (𝜑 → (𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))) |
37 | 36 | imim1d 82 |
. . . . . . . . 9
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
38 | 35, 37 | alimd 2212 |
. . . . . . . 8
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
39 | 33, 38 | alimd 2212 |
. . . . . . 7
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
40 | 39 | com12 32 |
. . . . . 6
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
41 | 40 | aleximi 1839 |
. . . . 5
⊢
(∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
42 | 41 | aleximi 1839 |
. . . 4
⊢
(∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
43 | | 2nexaln 1837 |
. . . . . 6
⊢ (¬
∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑) |
44 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑤𝜑 |
45 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑧𝜑 |
46 | 44, 45 | 2sb8ev 2357 |
. . . . . 6
⊢
(∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
47 | 43, 46 | xchnxbi 335 |
. . . . 5
⊢ (¬
∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑) |
48 | | pm2.21 123 |
. . . . . . . . 9
⊢ (¬
𝜑 → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
49 | 48 | 2alimi 1820 |
. . . . . . . 8
⊢
(∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
50 | 49 | 2eximi 1843 |
. . . . . . 7
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
51 | 50 | 19.23bi 2190 |
. . . . . 6
⊢
(∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
52 | 51 | 19.23bi 2190 |
. . . . 5
⊢
(∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
53 | 47, 52 | sylbi 220 |
. . . 4
⊢ (¬
∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
54 | 42, 53 | pm2.61d1 183 |
. . 3
⊢
(∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
55 | 32, 54 | impbii 212 |
. 2
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
56 | | alrot4 2164 |
. 2
⊢
(∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
57 | 55, 56 | bitri 278 |
1
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |