Step | Hyp | Ref
| Expression |
1 | | df-rel 4352 |
. 2
⊢ (Rel
〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉 ⊆ (V ×
V)) |
2 | | dfss2 2934 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
↔ ∀𝑧(𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V))) |
3 | | vex 2560 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
4 | | relop.1 |
. . . . . . . . . 10
⊢ 𝐴 ∈ V |
5 | | relop.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
6 | 3, 4, 5 | elop 3968 |
. . . . . . . . 9
⊢ (𝑧 ∈ 〈𝐴, 𝐵〉 ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) |
7 | | elvv 4402 |
. . . . . . . . 9
⊢ (𝑧 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) |
8 | 6, 7 | imbi12i 228 |
. . . . . . . 8
⊢ ((𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) |
9 | | jaob 631 |
. . . . . . . 8
⊢ (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
10 | 8, 9 | bitri 173 |
. . . . . . 7
⊢ ((𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
11 | 10 | albii 1359 |
. . . . . 6
⊢
(∀𝑧(𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
12 | | 19.26 1370 |
. . . . . 6
⊢
(∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
13 | 11, 12 | bitri 173 |
. . . . 5
⊢
(∀𝑧(𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
14 | 2, 13 | bitri 173 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉))) |
15 | | snexgOLD 3935 |
. . . . . . . 8
⊢ (𝐴 ∈ V → {𝐴} ∈ V) |
16 | 4, 15 | ax-mp 7 |
. . . . . . 7
⊢ {𝐴} ∈ V |
17 | | eqeq1 2046 |
. . . . . . . 8
⊢ (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴})) |
18 | | eqeq1 2046 |
. . . . . . . . . 10
⊢ (𝑧 = {𝐴} → (𝑧 = 〈𝑥, 𝑦〉 ↔ {𝐴} = 〈𝑥, 𝑦〉)) |
19 | | eqcom 2042 |
. . . . . . . . . . 11
⊢ ({𝐴} = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = {𝐴}) |
20 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
21 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
22 | 20, 21, 4 | opeqsn 3989 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 = {𝐴} ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) |
23 | 19, 22 | bitri 173 |
. . . . . . . . . 10
⊢ ({𝐴} = 〈𝑥, 𝑦〉 ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) |
24 | 18, 23 | syl6bb 185 |
. . . . . . . . 9
⊢ (𝑧 = {𝐴} → (𝑧 = 〈𝑥, 𝑦〉 ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
25 | 24 | 2exbidv 1748 |
. . . . . . . 8
⊢ (𝑧 = {𝐴} → (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
26 | 17, 25 | imbi12d 223 |
. . . . . . 7
⊢ (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))) |
27 | 16, 26 | spcv 2646 |
. . . . . 6
⊢
(∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
28 | | sneq 3386 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → {𝑤} = {𝑥}) |
29 | 28 | eqeq2d 2051 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥})) |
30 | 29 | cbvexv 1795 |
. . . . . . 7
⊢
(∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥}) |
31 | | a9ev 1587 |
. . . . . . . . . 10
⊢
∃𝑦 𝑦 = 𝑥 |
32 | | equcom 1593 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
33 | 32 | exbii 1496 |
. . . . . . . . . 10
⊢
(∃𝑦 𝑦 = 𝑥 ↔ ∃𝑦 𝑥 = 𝑦) |
34 | 31, 33 | mpbi 133 |
. . . . . . . . 9
⊢
∃𝑦 𝑥 = 𝑦 |
35 | | 19.41v 1782 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) |
36 | 34, 35 | mpbiran 847 |
. . . . . . . 8
⊢
(∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ 𝐴 = {𝑥}) |
37 | 36 | exbii 1496 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥}) |
38 | | eqid 2040 |
. . . . . . . 8
⊢ {𝐴} = {𝐴} |
39 | 38 | a1bi 232 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))) |
40 | 30, 37, 39 | 3bitr2ri 198 |
. . . . . 6
⊢ (({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤}) |
41 | 27, 40 | sylib 127 |
. . . . 5
⊢
(∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ∃𝑤 𝐴 = {𝑤}) |
42 | | eqid 2040 |
. . . . . 6
⊢ {𝐴, 𝐵} = {𝐴, 𝐵} |
43 | | prexgOLD 3946 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V) |
44 | 4, 5, 43 | mp2an 402 |
. . . . . . 7
⊢ {𝐴, 𝐵} ∈ V |
45 | | eqeq1 2046 |
. . . . . . . 8
⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵})) |
46 | | eqeq1 2046 |
. . . . . . . . 9
⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = 〈𝑥, 𝑦〉 ↔ {𝐴, 𝐵} = 〈𝑥, 𝑦〉)) |
47 | 46 | 2exbidv 1748 |
. . . . . . . 8
⊢ (𝑧 = {𝐴, 𝐵} → (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉)) |
48 | 45, 47 | imbi12d 223 |
. . . . . . 7
⊢ (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉))) |
49 | 44, 48 | spcv 2646 |
. . . . . 6
⊢
(∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉)) |
50 | 42, 49 | mpi 15 |
. . . . 5
⊢
(∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉) |
51 | | eqcom 2042 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = {𝐴, 𝐵}) |
52 | 20, 21, 4, 5 | opeqpr 3990 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}))) |
53 | 51, 52 | bitri 173 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} = 〈𝑥, 𝑦〉 ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}))) |
54 | | idd 21 |
. . . . . . . . . 10
⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
55 | | eqtr2 2058 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤}) |
56 | | vex 2560 |
. . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V |
57 | 20, 21, 56 | preqsn 3546 |
. . . . . . . . . . . . . . 15
⊢ ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦 ∧ 𝑦 = 𝑤)) |
58 | 57 | simplbi 259 |
. . . . . . . . . . . . . 14
⊢ ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦) |
59 | 55, 58 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦) |
60 | | dfsn2 3389 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑥} = {𝑥, 𝑥} |
61 | | preq2 3448 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦}) |
62 | 60, 61 | syl5req 2085 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥}) |
63 | 62 | eqeq2d 2051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥})) |
64 | 60, 61 | syl5eq 2084 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦}) |
65 | 64 | eqeq2d 2051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦})) |
66 | 63, 65 | anbi12d 442 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
67 | 66 | biimpd 132 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
68 | 67 | expd 245 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
69 | 68 | com12 27 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
70 | 69 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
71 | 59, 70 | mpd 13 |
. . . . . . . . . . . 12
⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
72 | 71 | expcom 109 |
. . . . . . . . . . 11
⊢ (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))) |
73 | 72 | impd 242 |
. . . . . . . . . 10
⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
74 | 54, 73 | jaod 637 |
. . . . . . . . 9
⊢ (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
75 | 53, 74 | syl5bi 141 |
. . . . . . . 8
⊢ (𝐴 = {𝑤} → ({𝐴, 𝐵} = 〈𝑥, 𝑦〉 → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
76 | 75 | 2eximdv 1762 |
. . . . . . 7
⊢ (𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉 → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
77 | 76 | exlimiv 1489 |
. . . . . 6
⊢
(∃𝑤 𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉 → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))) |
78 | 77 | imp 115 |
. . . . 5
⊢
((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥∃𝑦{𝐴, 𝐵} = 〈𝑥, 𝑦〉) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
79 | 41, 50, 78 | syl2an 273 |
. . . 4
⊢
((∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
80 | 14, 79 | sylbi 114 |
. . 3
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
→ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
81 | | simpr 103 |
. . . . . . . . . . 11
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴}) |
82 | | equid 1589 |
. . . . . . . . . . . . . 14
⊢ 𝑥 = 𝑥 |
83 | 82 | jctl 297 |
. . . . . . . . . . . . 13
⊢ (𝐴 = {𝑥} → (𝑥 = 𝑥 ∧ 𝐴 = {𝑥})) |
84 | 20, 20, 4 | opeqsn 3989 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑥〉 = {𝐴} ↔ (𝑥 = 𝑥 ∧ 𝐴 = {𝑥})) |
85 | 83, 84 | sylibr 137 |
. . . . . . . . . . . 12
⊢ (𝐴 = {𝑥} → 〈𝑥, 𝑥〉 = {𝐴}) |
86 | 85 | adantr 261 |
. . . . . . . . . . 11
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 〈𝑥, 𝑥〉 = {𝐴}) |
87 | 81, 86 | eqtr4d 2075 |
. . . . . . . . . 10
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = 〈𝑥, 𝑥〉) |
88 | | opeq12 3551 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → 〈𝑤, 𝑣〉 = 〈𝑥, 𝑥〉) |
89 | 88 | eqeq2d 2051 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → (𝑧 = 〈𝑤, 𝑣〉 ↔ 𝑧 = 〈𝑥, 𝑥〉)) |
90 | 20, 20, 89 | spc2ev 2648 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑥〉 → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
91 | 87, 90 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
92 | 91 | adantlr 446 |
. . . . . . . 8
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
93 | | preq12 3449 |
. . . . . . . . . . . 12
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}}) |
94 | 93 | eqeq2d 2051 |
. . . . . . . . . . 11
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}})) |
95 | 94 | biimpa 280 |
. . . . . . . . . 10
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}}) |
96 | 20, 21 | dfop 3548 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑦〉 = {{𝑥}, {𝑥, 𝑦}} |
97 | 95, 96 | syl6eqr 2090 |
. . . . . . . . 9
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = 〈𝑥, 𝑦〉) |
98 | | opeq12 3551 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑤, 𝑣〉 = 〈𝑥, 𝑦〉) |
99 | 98 | eqeq2d 2051 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑧 = 〈𝑤, 𝑣〉 ↔ 𝑧 = 〈𝑥, 𝑦〉)) |
100 | 20, 21, 99 | spc2ev 2648 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
101 | 97, 100 | syl 14 |
. . . . . . . 8
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
102 | 92, 101 | jaodan 710 |
. . . . . . 7
⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
103 | 102 | ex 108 |
. . . . . 6
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉)) |
104 | | elvv 4402 |
. . . . . 6
⊢ (𝑧 ∈ (V × V) ↔
∃𝑤∃𝑣 𝑧 = 〈𝑤, 𝑣〉) |
105 | 103, 6, 104 | 3imtr4g 194 |
. . . . 5
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ 〈𝐴, 𝐵〉 → 𝑧 ∈ (V × V))) |
106 | 105 | ssrdv 2951 |
. . . 4
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → 〈𝐴, 𝐵〉 ⊆ (V ×
V)) |
107 | 106 | exlimivv 1776 |
. . 3
⊢
(∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → 〈𝐴, 𝐵〉 ⊆ (V ×
V)) |
108 | 80, 107 | impbii 117 |
. 2
⊢
(〈𝐴, 𝐵〉 ⊆ (V × V)
↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
109 | 1, 108 | bitri 173 |
1
⊢ (Rel
〈𝐴, 𝐵〉 ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |