Step | Hyp | Ref
| Expression |
1 | | notnotb 314 |
. . . . . . 7
⊢
(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ¬ ¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) |
2 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑐(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) |
3 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) |
4 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑎⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ |
5 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑎 𝑐 ≠ 𝑑 |
6 | | nfsbc1v 3759 |
. . . . . . . . . 10
⊢
Ⅎ𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑 |
7 | 4, 5, 6 | nf3an 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
8 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑏⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ |
9 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑏 𝑐 ≠ 𝑑 |
10 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏𝑐 |
11 | | nfsbc1v 3759 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏[𝑑 / 𝑏]𝜑 |
12 | 10, 11 | nfsbcw 3761 |
. . . . . . . . . 10
⊢
Ⅎ𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑 |
13 | 8, 9, 12 | nf3an 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
14 | | opeq12 4832 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩) |
15 | 14 | eqeq2d 2747 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩)) |
16 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑎 = 𝑐) |
17 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑏 = 𝑑) |
18 | 16, 17 | neeq12d 3005 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 ≠ 𝑏 ↔ 𝑐 ≠ 𝑑)) |
19 | | sbceq1a 3750 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑏]𝜑)) |
20 | | sbceq1a 3750 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) |
21 | 19, 20 | sylan9bbr 511 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) |
22 | 15, 18, 21 | 3anbi123d 1436 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))) |
23 | 2, 3, 7, 13, 22 | cbvex2v 2340 |
. . . . . . . 8
⊢
(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑐∃𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) |
24 | | vex 3449 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
25 | | vex 3449 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
26 | 24, 25 | opth 5433 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐 ∧ 𝑦 = 𝑑)) |
27 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑑 → (𝑦 ∈ 𝑋 ↔ 𝑑 ∈ 𝑋)) |
28 | 27 | biimpcd 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑋 → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋)) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋)) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋)) |
31 | 30 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋)) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋)) |
33 | 26, 32 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋)) |
34 | 33 | 3ad2ant1 1133 |
. . . . . . . . . . . . 13
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋)) |
35 | 34 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ∈ 𝑋) |
36 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑐 → (𝑥 ∈ 𝑋 ↔ 𝑐 ∈ 𝑋)) |
37 | 36 | biimpcd 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑋 → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋)) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋)) |
39 | 38 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋)) |
40 | 39 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑐 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋)) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋)) |
42 | 26, 41 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋)) |
43 | 42 | 3ad2ant1 1133 |
. . . . . . . . . . . . 13
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋)) |
44 | 43 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐 ∈ 𝑋) |
45 | | eqidd 2737 |
. . . . . . . . . . . . . . . 16
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩) |
46 | | necom 2997 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ≠ 𝑑 ↔ 𝑑 ≠ 𝑐) |
47 | 46 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ≠ 𝑑 → 𝑑 ≠ 𝑐) |
48 | 47 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . 17
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑 ≠ 𝑐) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ≠ 𝑐) |
50 | | dfich2 45640 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
51 | | 2sp 2179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
52 | | sbsbc 3743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑) |
53 | 52 | sbbii 2079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
54 | | sbsbc 3743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
55 | 53, 54 | bitri 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
56 | | sbsbc 3743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑐 / 𝑏]𝜑 ↔ [𝑐 / 𝑏]𝜑) |
57 | 56 | sbbii 2079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
58 | | sbsbc 3743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
59 | 57, 58 | bitri 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
60 | 51, 55, 59 | 3bitr3g 312 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
61 | 60 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
62 | 50, 61 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ([𝑎⇄𝑏]𝜑 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
64 | 63 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢
([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
65 | 64 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . 18
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
66 | 65 | impcom 408 |
. . . . . . . . . . . . . . . . 17
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
67 | | sbccom 3827 |
. . . . . . . . . . . . . . . . 17
⊢
([𝑐 / 𝑏][𝑑 / 𝑎]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
68 | 66, 67 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) |
69 | 45, 49, 68 | 3jca 1128 |
. . . . . . . . . . . . . . 15
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)) |
70 | | nfv 1917 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑏⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ |
71 | | nfv 1917 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑏 𝑑 ≠ 𝑐 |
72 | | nfsbc1v 3759 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑 |
73 | 70, 71, 72 | nf3an 1904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) |
74 | | opeq2 4831 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩) |
75 | 74 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)) |
76 | | neeq2 3007 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → (𝑑 ≠ 𝑏 ↔ 𝑑 ≠ 𝑐)) |
77 | | sbceq1a 3750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑 ↔ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)) |
78 | 75, 76, 77 | 3anbi123d 1436 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))) |
79 | 10, 73, 78 | spcegf 3551 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))) |
80 | 44, 69, 79 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)) |
81 | | nfcv 2907 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑎𝑑 |
82 | | nfv 1917 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ |
83 | | nfv 1917 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎 𝑑 ≠ 𝑏 |
84 | | nfsbc1v 3759 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎[𝑑 / 𝑎]𝜑 |
85 | 82, 83, 84 | nf3an 1904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) |
86 | 85 | nfex 2317 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) |
87 | | opeq1 4830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩) |
88 | 87 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩)) |
89 | | neeq1 3006 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑑 → (𝑎 ≠ 𝑏 ↔ 𝑑 ≠ 𝑏)) |
90 | | sbceq1a 3750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑎]𝜑)) |
91 | 88, 89, 90 | 3anbi123d 1436 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))) |
92 | 91 | exbidv 1924 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))) |
93 | 81, 86, 92 | spcegf 3551 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
94 | 35, 80, 93 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) |
95 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑑 ∈ V |
96 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑐 ∈ V |
97 | 95, 96 | opth1 5432 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐) |
98 | 97 | equcomd 2022 |
. . . . . . . . . . . . . . . . . 18
⊢
(⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑) |
99 | 98 | necon3ai 2968 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ≠ 𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩) |
100 | 99 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩) |
101 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . 17
⊢
(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)) |
103 | 100, 102 | mtbird 324 |
. . . . . . . . . . . . . . 15
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩) |
104 | 103 | 3adant3 1132 |
. . . . . . . . . . . . . 14
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩) |
105 | 104 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩) |
106 | 94, 105 | jcnd 163 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) |
107 | | opeq1 4830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩) |
108 | 107 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩)) |
109 | 108 | 3anbi1d 1440 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
110 | 109 | 2exbidv 1927 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑑 → (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
111 | 107 | eqeq1d 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) |
112 | 110, 111 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑑 → ((∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
113 | 112 | notbid 317 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑑 → (¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
114 | | opeq2 4831 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩) |
115 | 114 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩)) |
116 | 115 | 3anbi1d 1440 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
117 | 116 | 2exbidv 1927 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑐 → (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
118 | 114 | eqeq1d 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) |
119 | 117, 118 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑐 → ((∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))) |
120 | 119 | notbid 317 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑐 → (¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))) |
121 | 113, 120 | rspc2ev 3592 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) |
122 | 35, 44, 106, 121 | syl3anc 1371 |
. . . . . . . . . . 11
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) |
123 | | rexnal2 3132 |
. . . . . . . . . . 11
⊢
(∃𝑣 ∈
𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) |
124 | 122, 123 | sylib 217 |
. . . . . . . . . 10
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) |
125 | 124 | ex 413 |
. . . . . . . . 9
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
126 | 125 | exlimdvv 1937 |
. . . . . . . 8
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑐∃𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
127 | 23, 126 | biimtrid 241 |
. . . . . . 7
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
128 | 1, 127 | biimtrrid 242 |
. . . . . 6
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
129 | 128 | orrd 861 |
. . . . 5
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
130 | | ianor 980 |
. . . . 5
⊢ (¬
(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
131 | 129, 130 | sylibr 233 |
. . . 4
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
132 | 131 | ralrimivva 3197 |
. . 3
⊢ ([𝑎⇄𝑏]𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
133 | | ralnex2 3130 |
. . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
134 | 132, 133 | sylib 217 |
. 2
⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
135 | | eqeq1 2740 |
. . . . 5
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) |
136 | 135 | 3anbi1d 1440 |
. . . 4
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
137 | 136 | 2exbidv 1927 |
. . 3
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
138 | | eqeq1 2740 |
. . . . 5
⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩)) |
139 | 138 | 3anbi1d 1440 |
. . . 4
⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
140 | 139 | 2exbidv 1927 |
. . 3
⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
141 | 137, 140 | reuop 6245 |
. 2
⊢
(∃!𝑝 ∈
(𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))) |
142 | 134, 141 | sylnibr 328 |
1
⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) |