Step | Hyp | Ref
| Expression |
1 | | notnotb 315 |
. . . . . . 7
⊢
(∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ¬ ¬ ∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) |
2 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑐(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) |
3 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑑(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) |
4 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑎〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 |
5 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑎 𝑐 ≠ 𝑑 |
6 | | nfsbc1v 3740 |
. . . . . . . . . 10
⊢
Ⅎ𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑 |
7 | 4, 5, 6 | nf3an 1908 |
. . . . . . . . 9
⊢
Ⅎ𝑎(〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
8 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑏〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 |
9 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑏 𝑐 ≠ 𝑑 |
10 | | nfcv 2909 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏𝑐 |
11 | | nfsbc1v 3740 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏[𝑑 / 𝑏]𝜑 |
12 | 10, 11 | nfsbcw 3742 |
. . . . . . . . . 10
⊢
Ⅎ𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑 |
13 | 8, 9, 12 | nf3an 1908 |
. . . . . . . . 9
⊢
Ⅎ𝑏(〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
14 | | opeq12 4812 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 〈𝑎, 𝑏〉 = 〈𝑐, 𝑑〉) |
15 | 14 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ↔ 〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉)) |
16 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑎 = 𝑐) |
17 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑏 = 𝑑) |
18 | 16, 17 | neeq12d 3007 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 ≠ 𝑏 ↔ 𝑐 ≠ 𝑑)) |
19 | | sbceq1a 3731 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑏]𝜑)) |
20 | | sbceq1a 3731 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) |
21 | 19, 20 | sylan9bbr 511 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) |
22 | 15, 18, 21 | 3anbi123d 1435 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ((〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))) |
23 | 2, 3, 7, 13, 22 | cbvex2v 2346 |
. . . . . . . 8
⊢
(∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑐∃𝑑(〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) |
24 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
25 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
26 | 24, 25 | opth 5395 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ↔ (𝑥 = 𝑐 ∧ 𝑦 = 𝑑)) |
27 | | eleq1w 2823 |
. . . . . . . . . . . . . . . . . . . 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 1132 |
. . . . . . . . . . . . 13
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋)) |
35 | 34 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ∈ 𝑋) |
36 | | eleq1w 2823 |
. . . . . . . . . . . . . . . . . . . 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 1132 |
. . . . . . . . . . . . 13
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋)) |
44 | 43 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐 ∈ 𝑋) |
45 | | eqidd 2741 |
. . . . . . . . . . . . . . . 16
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 〈𝑑, 𝑐〉 = 〈𝑑, 𝑐〉) |
46 | | necom 2999 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ≠ 𝑑 ↔ 𝑑 ≠ 𝑐) |
47 | 46 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ≠ 𝑑 → 𝑑 ≠ 𝑐) |
48 | 47 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑 ≠ 𝑐) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ≠ 𝑐) |
50 | | dfich2 44879 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
51 | | 2sp 2183 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
52 | | sbsbc 3724 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑) |
53 | 52 | sbbii 2083 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
54 | | sbsbc 3724 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
55 | 53, 54 | bitri 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) |
56 | | sbsbc 3724 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑐 / 𝑏]𝜑 ↔ [𝑐 / 𝑏]𝜑) |
57 | 56 | sbbii 2083 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
58 | | sbsbc 3724 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
59 | 57, 58 | bitri 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
60 | 51, 55, 59 | 3bitr3g 313 |
. . . . . . . . . . . . . . . . . . . . . . 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 1134 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)) |
66 | 65 | impcom 408 |
. . . . . . . . . . . . . . . . 17
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
67 | | sbccom 3809 |
. . . . . . . . . . . . . . . . 17
⊢
([𝑐 / 𝑏][𝑑 / 𝑎]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) |
68 | 66, 67 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) |
69 | 45, 49, 68 | 3jca 1127 |
. . . . . . . . . . . . . . 15
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (〈𝑑, 𝑐〉 = 〈𝑑, 𝑐〉 ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)) |
70 | | nfv 1921 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑏〈𝑑, 𝑐〉 = 〈𝑑, 𝑐〉 |
71 | | nfv 1921 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑏 𝑑 ≠ 𝑐 |
72 | | nfsbc1v 3740 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑 |
73 | 70, 71, 72 | nf3an 1908 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑏(〈𝑑, 𝑐〉 = 〈𝑑, 𝑐〉 ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) |
74 | | opeq2 4811 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑐 → 〈𝑑, 𝑏〉 = 〈𝑑, 𝑐〉) |
75 | 74 | eqeq2d 2751 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → (〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ↔ 〈𝑑, 𝑐〉 = 〈𝑑, 𝑐〉)) |
76 | | neeq2 3009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → (𝑑 ≠ 𝑏 ↔ 𝑑 ≠ 𝑐)) |
77 | | sbceq1a 3731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑 ↔ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)) |
78 | 75, 76, 77 | 3anbi123d 1435 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑐 → ((〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) ↔ (〈𝑑, 𝑐〉 = 〈𝑑, 𝑐〉 ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))) |
79 | 10, 73, 78 | spcegf 3530 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝑋 → ((〈𝑑, 𝑐〉 = 〈𝑑, 𝑐〉 ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))) |
80 | 44, 69, 79 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)) |
81 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑎𝑑 |
82 | | nfv 1921 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 |
83 | | nfv 1921 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎 𝑑 ≠ 𝑏 |
84 | | nfsbc1v 3740 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎[𝑑 / 𝑎]𝜑 |
85 | 82, 83, 84 | nf3an 1908 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑎(〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) |
86 | 85 | nfex 2322 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) |
87 | | opeq1 4810 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑑 → 〈𝑎, 𝑏〉 = 〈𝑑, 𝑏〉) |
88 | 87 | eqeq2d 2751 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑑 → (〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ↔ 〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉)) |
89 | | neeq1 3008 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑑 → (𝑎 ≠ 𝑏 ↔ 𝑑 ≠ 𝑏)) |
90 | | sbceq1a 3731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑎]𝜑)) |
91 | 88, 89, 90 | 3anbi123d 1435 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑑 → ((〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))) |
92 | 91 | exbidv 1928 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑑 → (∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑏(〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))) |
93 | 81, 86, 92 | spcegf 3530 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝑋 → (∃𝑏(〈𝑑, 𝑐〉 = 〈𝑑, 𝑏〉 ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) → ∃𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
94 | 35, 80, 93 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) |
95 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑑 ∈ V |
96 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑐 ∈ V |
97 | 95, 96 | opth1 5394 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑑, 𝑐〉 = 〈𝑐, 𝑑〉 → 𝑑 = 𝑐) |
98 | 97 | equcomd 2026 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑑, 𝑐〉 = 〈𝑐, 𝑑〉 → 𝑐 = 𝑑) |
99 | 98 | necon3ai 2970 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ≠ 𝑑 → ¬ 〈𝑑, 𝑐〉 = 〈𝑐, 𝑑〉) |
100 | 99 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑) → ¬ 〈𝑑, 𝑐〉 = 〈𝑐, 𝑑〉) |
101 | | eqeq2 2752 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 → (〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑑, 𝑐〉 = 〈𝑐, 𝑑〉)) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑) → (〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑑, 𝑐〉 = 〈𝑐, 𝑑〉)) |
103 | 100, 102 | mtbird 325 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑) → ¬ 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉) |
104 | 103 | 3adant3 1131 |
. . . . . . . . . . . . . 14
⊢
((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉) |
105 | 104 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉) |
106 | 94, 105 | jcnd 163 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉)) |
107 | | opeq1 4810 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑑 → 〈𝑣, 𝑤〉 = 〈𝑑, 𝑤〉) |
108 | 107 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑑 → (〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ↔ 〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉)) |
109 | 108 | 3anbi1d 1439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑑 → ((〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
110 | 109 | 2exbidv 1931 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑑 → (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
111 | 107 | eqeq1d 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑑 → (〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑑, 𝑤〉 = 〈𝑥, 𝑦〉)) |
112 | 110, 111 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑑 → ((∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) ↔ (∃𝑎∃𝑏(〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑤〉 = 〈𝑥, 𝑦〉))) |
113 | 112 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑑 → (¬ (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) ↔ ¬ (∃𝑎∃𝑏(〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑤〉 = 〈𝑥, 𝑦〉))) |
114 | | opeq2 4811 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑐 → 〈𝑑, 𝑤〉 = 〈𝑑, 𝑐〉) |
115 | 114 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑐 → (〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ↔ 〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉)) |
116 | 115 | 3anbi1d 1439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑐 → ((〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
117 | 116 | 2exbidv 1931 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑐 → (∃𝑎∃𝑏(〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
118 | 114 | eqeq1d 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑐 → (〈𝑑, 𝑤〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉)) |
119 | 117, 118 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑐 → ((∃𝑎∃𝑏(〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑤〉 = 〈𝑥, 𝑦〉) ↔ (∃𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉))) |
120 | 119 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑐 → (¬ (∃𝑎∃𝑏(〈𝑑, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑤〉 = 〈𝑥, 𝑦〉) ↔ ¬ (∃𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉))) |
121 | 113, 120 | rspc2ev 3573 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ ¬ (∃𝑎∃𝑏(〈𝑑, 𝑐〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑑, 𝑐〉 = 〈𝑥, 𝑦〉)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) |
122 | 35, 44, 106, 121 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) |
123 | | rexnal2 3189 |
. . . . . . . . . . 11
⊢
(∃𝑣 ∈
𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) ↔ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) |
124 | 122, 123 | sylib 217 |
. . . . . . . . . 10
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) |
125 | 124 | ex 413 |
. . . . . . . . 9
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
126 | 125 | exlimdvv 1941 |
. . . . . . . 8
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑐∃𝑑(〈𝑥, 𝑦〉 = 〈𝑐, 𝑑〉 ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
127 | 23, 126 | syl5bi 241 |
. . . . . . 7
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
128 | 1, 127 | syl5bir 242 |
. . . . . 6
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ¬ ∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
129 | 128 | orrd 860 |
. . . . 5
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
130 | | ianor 979 |
. . . . 5
⊢ (¬
(∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) ↔ (¬ ∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
131 | 129, 130 | sylibr 233 |
. . . 4
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ¬ (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
132 | 131 | ralrimivva 3117 |
. . 3
⊢ ([𝑎⇄𝑏]𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
133 | | ralnex2 3191 |
. . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) ↔ ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
134 | 132, 133 | sylib 217 |
. 2
⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
135 | | eqeq1 2744 |
. . . . 5
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝑝 = 〈𝑎, 𝑏〉 ↔ 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉)) |
136 | 135 | 3anbi1d 1439 |
. . . 4
⊢ (𝑝 = 〈𝑥, 𝑦〉 → ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
137 | 136 | 2exbidv 1931 |
. . 3
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
138 | | eqeq1 2744 |
. . . . 5
⊢ (𝑝 = 〈𝑣, 𝑤〉 → (𝑝 = 〈𝑎, 𝑏〉 ↔ 〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉)) |
139 | 138 | 3anbi1d 1439 |
. . . 4
⊢ (𝑝 = 〈𝑣, 𝑤〉 → ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
140 | 139 | 2exbidv 1931 |
. . 3
⊢ (𝑝 = 〈𝑣, 𝑤〉 → (∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))) |
141 | 137, 140 | reuop 6195 |
. 2
⊢
(∃!𝑝 ∈
(𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
142 | 134, 141 | sylnibr 329 |
1
⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) |