Step | Hyp | Ref
| Expression |
1 | | eqeq1 2741 |
. . . . 5
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝑝 = 〈𝑎, 𝑏〉 ↔ 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉)) |
2 | 1 | anbi1d 633 |
. . . 4
⊢ (𝑝 = 〈𝑥, 𝑦〉 → ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) |
3 | 2 | 2exbidv 1932 |
. . 3
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) |
4 | | eqeq1 2741 |
. . . . 5
⊢ (𝑝 = 〈𝑣, 𝑤〉 → (𝑝 = 〈𝑎, 𝑏〉 ↔ 〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉)) |
5 | 4 | anbi1d 633 |
. . . 4
⊢ (𝑝 = 〈𝑣, 𝑤〉 → ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ (〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) |
6 | 5 | 2exbidv 1932 |
. . 3
⊢ (𝑝 = 〈𝑣, 𝑤〉 → (∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) |
7 | 3, 6 | reuop 6156 |
. 2
⊢
(∃!𝑝 ∈
(𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉))) |
8 | | nfich1 44572 |
. . . . . 6
⊢
Ⅎ𝑎[𝑎⇄𝑏]𝜑 |
9 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑎(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) |
10 | 8, 9 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑎([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
11 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑎𝑋 |
12 | | nfe1 2151 |
. . . . . . . . 9
⊢
Ⅎ𝑎∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) |
13 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑎〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉 |
14 | 12, 13 | nfim 1904 |
. . . . . . . 8
⊢
Ⅎ𝑎(∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) |
15 | 11, 14 | nfralw 3147 |
. . . . . . 7
⊢
Ⅎ𝑎∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) |
16 | 11, 15 | nfralw 3147 |
. . . . . 6
⊢
Ⅎ𝑎∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) |
17 | | nfe1 2151 |
. . . . . 6
⊢
Ⅎ𝑎∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑) |
18 | 16, 17 | nfim 1904 |
. . . . 5
⊢
Ⅎ𝑎(∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)) |
19 | | nfich2 44573 |
. . . . . . 7
⊢
Ⅎ𝑏[𝑎⇄𝑏]𝜑 |
20 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑏(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) |
21 | 19, 20 | nfan 1907 |
. . . . . 6
⊢
Ⅎ𝑏([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
22 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑏𝑋 |
23 | | nfe1 2151 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) |
24 | 23 | nfex 2323 |
. . . . . . . . . 10
⊢
Ⅎ𝑏∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) |
25 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑏〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉 |
26 | 24, 25 | nfim 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑏(∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) |
27 | 22, 26 | nfralw 3147 |
. . . . . . . 8
⊢
Ⅎ𝑏∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) |
28 | 22, 27 | nfralw 3147 |
. . . . . . 7
⊢
Ⅎ𝑏∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) |
29 | | nfe1 2151 |
. . . . . . . 8
⊢
Ⅎ𝑏∃𝑏(𝑎 = 𝑏 ∧ 𝜑) |
30 | 29 | nfex 2323 |
. . . . . . 7
⊢
Ⅎ𝑏∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑) |
31 | 28, 30 | nfim 1904 |
. . . . . 6
⊢
Ⅎ𝑏(∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)) |
32 | | opeq12 4786 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 = 𝑦 ∧ 𝑤 = 𝑥) → 〈𝑣, 𝑤〉 = 〈𝑦, 𝑥〉) |
33 | 32 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ ((𝑣 = 𝑦 ∧ 𝑤 = 𝑥) → (〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉)) |
34 | 33 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ ((𝑣 = 𝑦 ∧ 𝑤 = 𝑥) → ((〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ (〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) |
35 | 34 | 2exbidv 1932 |
. . . . . . . . . . 11
⊢ ((𝑣 = 𝑦 ∧ 𝑤 = 𝑥) → (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) |
36 | 32 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((𝑣 = 𝑦 ∧ 𝑤 = 𝑥) → (〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉)) |
37 | 35, 36 | imbi12d 348 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑦 ∧ 𝑤 = 𝑥) → ((∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) ↔ (∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉))) |
38 | 37 | rspc2gv 3546 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → (∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉))) |
39 | 38 | ancoms 462 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → (∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉))) |
40 | 39 | adantl 485 |
. . . . . . 7
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → (∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉))) |
41 | | simprr 773 |
. . . . . . . . . . 11
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
42 | 41 | adantr 484 |
. . . . . . . . . 10
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → 𝑦 ∈ 𝑋) |
43 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
44 | 43 | adantl 485 |
. . . . . . . . . . . 12
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
45 | 44 | adantr 484 |
. . . . . . . . . . 11
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → 𝑥 ∈ 𝑋) |
46 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → 〈𝑦, 𝑥〉 = 〈𝑦, 𝑥〉) |
47 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
48 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
49 | 47, 48 | opth 5360 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ↔ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) |
50 | | sbceq1a 3705 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑏]𝜑)) |
51 | 50 | equcoms 2028 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑏 → (𝜑 ↔ [𝑦 / 𝑏]𝜑)) |
52 | | sbceq1a 3705 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑥 → ([𝑦 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑)) |
53 | 52 | equcoms 2028 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ([𝑦 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑)) |
54 | 51, 53 | sylan9bbr 514 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑)) |
55 | | dfich2 44583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
56 | | 2sp 2183 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
57 | | sbsbc 3698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ([𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑏]𝜑) |
58 | 57 | sbbii 2082 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑) |
59 | | sbsbc 3698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑) |
60 | 58, 59 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑) |
61 | | sbsbc 3698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ([𝑥 / 𝑏]𝜑 ↔ [𝑥 / 𝑏]𝜑) |
62 | 61 | sbbii 2082 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) |
63 | | sbsbc 3698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) |
64 | 62, 63 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) |
65 | 56, 60, 64 | 3bitr3g 316 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
66 | 55, 65 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ([𝑎⇄𝑏]𝜑 → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
67 | 66 | biimpd 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑎⇄𝑏]𝜑 → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
68 | 67 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
69 | 68 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
70 | 54, 69 | syl6bi 256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))) |
71 | 49, 70 | sylbi 220 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 → (𝜑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))) |
72 | 71 | imp 410 |
. . . . . . . . . . . . . 14
⊢
((〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)) |
73 | 72 | impcom 411 |
. . . . . . . . . . . . 13
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) |
74 | | sbccom 3783 |
. . . . . . . . . . . . 13
⊢
([𝑥 / 𝑏][𝑦 / 𝑎]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) |
75 | 73, 74 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → [𝑥 / 𝑏][𝑦 / 𝑎]𝜑) |
76 | 46, 75 | jca 515 |
. . . . . . . . . . 11
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → (〈𝑦, 𝑥〉 = 〈𝑦, 𝑥〉 ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)) |
77 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏𝑥 |
78 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑏〈𝑦, 𝑥〉 = 〈𝑦, 𝑥〉 |
79 | | nfsbc1v 3714 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑏[𝑥 / 𝑏][𝑦 / 𝑎]𝜑 |
80 | 78, 79 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏(〈𝑦, 𝑥〉 = 〈𝑦, 𝑥〉 ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑) |
81 | | opeq2 4785 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑥 → 〈𝑦, 𝑏〉 = 〈𝑦, 𝑥〉) |
82 | 81 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑥 → (〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑦, 𝑥〉)) |
83 | | sbceq1a 3705 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑥 → ([𝑦 / 𝑎]𝜑 ↔ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)) |
84 | 82, 83 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑥 → ((〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑) ↔ (〈𝑦, 𝑥〉 = 〈𝑦, 𝑥〉 ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑))) |
85 | 77, 80, 84 | spcegf 3507 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 → ((〈𝑦, 𝑥〉 = 〈𝑦, 𝑥〉 ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑) → ∃𝑏(〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑))) |
86 | 45, 76, 85 | sylc 65 |
. . . . . . . . . 10
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → ∃𝑏(〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑)) |
87 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎𝑦 |
88 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 |
89 | | nfsbc1v 3714 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎[𝑦 / 𝑎]𝜑 |
90 | 88, 89 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎(〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑) |
91 | 90 | nfex 2323 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑) |
92 | | opeq1 4784 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑦 → 〈𝑎, 𝑏〉 = 〈𝑦, 𝑏〉) |
93 | 92 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑦 → (〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉)) |
94 | | sbceq1a 3705 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑎]𝜑)) |
95 | 93, 94 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑦 → ((〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ (〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑))) |
96 | 95 | exbidv 1929 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑦 → (∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ ∃𝑏(〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑))) |
97 | 87, 91, 96 | spcegf 3507 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑋 → (∃𝑏(〈𝑦, 𝑥〉 = 〈𝑦, 𝑏〉 ∧ [𝑦 / 𝑎]𝜑) → ∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) |
98 | 42, 86, 97 | sylc 65 |
. . . . . . . . 9
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → ∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) |
99 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝑦 = 𝑥) |
100 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝑦 = 𝑏) |
101 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → 𝑥 = 𝑎) |
102 | 101 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝑥 = 𝑎) |
103 | 99, 100, 102 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝑎 = 𝑏) |
104 | 103 | anim1i 618 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑥 ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) ∧ 𝜑) → (𝑎 = 𝑏 ∧ 𝜑)) |
105 | 104 | exp31 423 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 → (𝑎 = 𝑏 ∧ 𝜑)))) |
106 | 49, 105 | syl5bi 245 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 → (𝜑 → (𝑎 = 𝑏 ∧ 𝜑)))) |
107 | 106 | impd 414 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ((〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → (𝑎 = 𝑏 ∧ 𝜑))) |
108 | 48, 47 | opth1 5359 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉 → 𝑦 = 𝑥) |
109 | 107, 108 | syl11 33 |
. . . . . . . . . . . . . 14
⊢
((〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → (〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉 → (𝑎 = 𝑏 ∧ 𝜑))) |
110 | 109 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → (〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉 → (𝑎 = 𝑏 ∧ 𝜑))) |
111 | 110 | imp 410 |
. . . . . . . . . . . 12
⊢
(((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) ∧ 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉) → (𝑎 = 𝑏 ∧ 𝜑)) |
112 | 111 | 19.8ad 2179 |
. . . . . . . . . . 11
⊢
(((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) ∧ 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉) → ∃𝑏(𝑎 = 𝑏 ∧ 𝜑)) |
113 | 112 | 19.8ad 2179 |
. . . . . . . . . 10
⊢
(((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) ∧ 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)) |
114 | 113 | ex 416 |
. . . . . . . . 9
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → (〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉 → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑))) |
115 | 98, 114 | embantd 59 |
. . . . . . . 8
⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑)) → ((∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑))) |
116 | 115 | ex 416 |
. . . . . . 7
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → ((∃𝑎∃𝑏(〈𝑦, 𝑥〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑦, 𝑥〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)))) |
117 | 40, 116 | syl5d 73 |
. . . . . 6
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → (∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)))) |
118 | 21, 31, 117 | exlimd 2216 |
. . . . 5
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → (∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)))) |
119 | 10, 18, 118 | exlimd 2216 |
. . . 4
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → (∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)))) |
120 | 119 | impd 414 |
. . 3
⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑))) |
121 | 120 | rexlimdvva 3213 |
. 2
⊢ ([𝑎⇄𝑏]𝜑 → (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(〈𝑣, 𝑤〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑦〉)) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑))) |
122 | 7, 121 | syl5bi 245 |
1
⊢ ([𝑎⇄𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑))) |