Step | Hyp | Ref
| Expression |
1 | | df-rel 4295 |
. 2
⊢ (Rel
〈A, B〉 ↔ 〈A, B〉
⊆ (V × V)) |
2 | | dfss2 2928 |
. . . . 5
⊢
(〈A, B〉 ⊆ (V × V) ↔ ∀z(z ∈ 〈A, B〉
→ z ∈ (V × V))) |
3 | | vex 2554 |
. . . . . . . . . 10
⊢ z ∈
V |
4 | | relop.1 |
. . . . . . . . . 10
⊢ A ∈
V |
5 | | relop.2 |
. . . . . . . . . 10
⊢ B ∈
V |
6 | 3, 4, 5 | elop 3959 |
. . . . . . . . 9
⊢ (z ∈ 〈A, B〉
↔ (z = {A} ∨ z = {A, B})) |
7 | | elvv 4345 |
. . . . . . . . 9
⊢ (z ∈ (V × V)
↔ ∃x∃y z =
〈x, y〉) |
8 | 6, 7 | imbi12i 228 |
. . . . . . . 8
⊢
((z ∈ 〈A,
B〉 → z ∈ (V × V))
↔ ((z = {A} ∨ z = {A, B}) → ∃x∃y z = 〈x,
y〉)) |
9 | | jaob 630 |
. . . . . . . 8
⊢
(((z = {A} ∨ z = {A, B}) → ∃x∃y z = 〈x,
y〉) ↔ ((z = {A} →
∃x∃y z = 〈x,
y〉) ∧
(z = {A, B} →
∃x∃y z = 〈x,
y〉))) |
10 | 8, 9 | bitri 173 |
. . . . . . 7
⊢
((z ∈ 〈A,
B〉 → z ∈ (V × V))
↔ ((z = {A} → ∃x∃y z = 〈x,
y〉) ∧
(z = {A, B} →
∃x∃y z = 〈x,
y〉))) |
11 | 10 | albii 1356 |
. . . . . 6
⊢ (∀z(z ∈ 〈A, B〉
→ z ∈ (V × V)) ↔ ∀z((z = {A} →
∃x∃y z = 〈x,
y〉) ∧
(z = {A, B} →
∃x∃y z = 〈x,
y〉))) |
12 | | 19.26 1367 |
. . . . . 6
⊢ (∀z((z = {A} →
∃x∃y z = 〈x,
y〉) ∧
(z = {A, B} →
∃x∃y z = 〈x,
y〉)) ↔ (∀z(z = {A} →
∃x∃y z = 〈x,
y〉) ∧
∀z(z = {A, B} →
∃x∃y z = 〈x,
y〉))) |
13 | 11, 12 | bitri 173 |
. . . . 5
⊢ (∀z(z ∈ 〈A, B〉
→ z ∈ (V × V)) ↔ (∀z(z = {A} →
∃x∃y z = 〈x,
y〉) ∧
∀z(z = {A, B} →
∃x∃y z = 〈x,
y〉))) |
14 | 2, 13 | bitri 173 |
. . . 4
⊢
(〈A, B〉 ⊆ (V × V) ↔ (∀z(z = {A} →
∃x∃y z = 〈x,
y〉) ∧
∀z(z = {A, B} →
∃x∃y z = 〈x,
y〉))) |
15 | | snexgOLD 3926 |
. . . . . . . 8
⊢ (A ∈ V →
{A} ∈
V) |
16 | 4, 15 | ax-mp 7 |
. . . . . . 7
⊢ {A} ∈
V |
17 | | eqeq1 2043 |
. . . . . . . 8
⊢ (z = {A} →
(z = {A} ↔ {A} =
{A})) |
18 | | eqeq1 2043 |
. . . . . . . . . 10
⊢ (z = {A} →
(z = 〈x, y〉
↔ {A} = 〈x, y〉)) |
19 | | eqcom 2039 |
. . . . . . . . . . 11
⊢
({A} = 〈x, y〉
↔ 〈x, y〉 = {A}) |
20 | | vex 2554 |
. . . . . . . . . . . 12
⊢ x ∈
V |
21 | | vex 2554 |
. . . . . . . . . . . 12
⊢ y ∈
V |
22 | 20, 21, 4 | opeqsn 3980 |
. . . . . . . . . . 11
⊢
(〈x, y〉 = {A}
↔ (x = y ∧ A = {x})) |
23 | 19, 22 | bitri 173 |
. . . . . . . . . 10
⊢
({A} = 〈x, y〉
↔ (x = y ∧ A = {x})) |
24 | 18, 23 | syl6bb 185 |
. . . . . . . . 9
⊢ (z = {A} →
(z = 〈x, y〉
↔ (x = y ∧ A = {x}))) |
25 | 24 | 2exbidv 1745 |
. . . . . . . 8
⊢ (z = {A} →
(∃x∃y z = 〈x,
y〉 ↔ ∃x∃y(x = y ∧ A = {x}))) |
26 | 17, 25 | imbi12d 223 |
. . . . . . 7
⊢ (z = {A} →
((z = {A} → ∃x∃y z = 〈x,
y〉) ↔ ({A} = {A} →
∃x∃y(x = y ∧ A = {x})))) |
27 | 16, 26 | spcv 2640 |
. . . . . 6
⊢ (∀z(z = {A} →
∃x∃y z = 〈x,
y〉) → ({A} = {A} →
∃x∃y(x = y ∧ A = {x}))) |
28 | | sneq 3378 |
. . . . . . . . 9
⊢ (w = x →
{w} = {x}) |
29 | 28 | eqeq2d 2048 |
. . . . . . . 8
⊢ (w = x →
(A = {w} ↔ A =
{x})) |
30 | 29 | cbvexv 1792 |
. . . . . . 7
⊢ (∃w A = {w} ↔
∃x
A = {x}) |
31 | | a9ev 1584 |
. . . . . . . . . 10
⊢ ∃y y = x |
32 | | equcom 1590 |
. . . . . . . . . . 11
⊢ (y = x ↔
x = y) |
33 | 32 | exbii 1493 |
. . . . . . . . . 10
⊢ (∃y y = x ↔
∃y
x = y) |
34 | 31, 33 | mpbi 133 |
. . . . . . . . 9
⊢ ∃y x = y |
35 | | 19.41v 1779 |
. . . . . . . . 9
⊢ (∃y(x = y ∧ A = {x}) ↔ (∃y x = y ∧ A = {x})) |
36 | 34, 35 | mpbiran 846 |
. . . . . . . 8
⊢ (∃y(x = y ∧ A = {x}) ↔ A =
{x}) |
37 | 36 | exbii 1493 |
. . . . . . 7
⊢ (∃x∃y(x = y ∧ A = {x}) ↔ ∃x A = {x}) |
38 | | eqid 2037 |
. . . . . . . 8
⊢ {A} = {A} |
39 | 38 | a1bi 232 |
. . . . . . 7
⊢ (∃x∃y(x = y ∧ A = {x}) ↔ ({A}
= {A} → ∃x∃y(x = y ∧ A = {x}))) |
40 | 30, 37, 39 | 3bitr2ri 198 |
. . . . . 6
⊢
(({A} = {A} → ∃x∃y(x = y ∧ A = {x})) ↔ ∃w A = {w}) |
41 | 27, 40 | sylib 127 |
. . . . 5
⊢ (∀z(z = {A} →
∃x∃y z = 〈x,
y〉) → ∃w A = {w}) |
42 | | eqid 2037 |
. . . . . 6
⊢ {A, B} =
{A, B} |
43 | | prexgOLD 3937 |
. . . . . . . 8
⊢
((A ∈ V ∧ B ∈ V) →
{A, B}
∈ V) |
44 | 4, 5, 43 | mp2an 402 |
. . . . . . 7
⊢ {A, B} ∈ V |
45 | | eqeq1 2043 |
. . . . . . . 8
⊢ (z = {A, B} → (z =
{A, B}
↔ {A, B} = {A,
B})) |
46 | | eqeq1 2043 |
. . . . . . . . 9
⊢ (z = {A, B} → (z =
〈x, y〉 ↔ {A, B} =
〈x, y〉)) |
47 | 46 | 2exbidv 1745 |
. . . . . . . 8
⊢ (z = {A, B} → (∃x∃y z = 〈x,
y〉 ↔ ∃x∃y{A, B} =
〈x, y〉)) |
48 | 45, 47 | imbi12d 223 |
. . . . . . 7
⊢ (z = {A, B} → ((z =
{A, B}
→ ∃x∃y z =
〈x, y〉) ↔ ({A, B} =
{A, B}
→ ∃x∃y{A, B} = 〈x,
y〉))) |
49 | 44, 48 | spcv 2640 |
. . . . . 6
⊢ (∀z(z = {A, B} → ∃x∃y z = 〈x,
y〉) → ({A, B} =
{A, B}
→ ∃x∃y{A, B} = 〈x,
y〉)) |
50 | 42, 49 | mpi 15 |
. . . . 5
⊢ (∀z(z = {A, B} → ∃x∃y z = 〈x,
y〉) → ∃x∃y{A, B} =
〈x, y〉) |
51 | | eqcom 2039 |
. . . . . . . . . 10
⊢
({A, B} = 〈x,
y〉 ↔ 〈x, y〉 =
{A, B}) |
52 | 20, 21, 4, 5 | opeqpr 3981 |
. . . . . . . . . 10
⊢
(〈x, y〉 = {A,
B} ↔ ((A = {x} ∧ B = {x, y}) ∨ (A = {x, y} ∧ B = {x}))) |
53 | 51, 52 | bitri 173 |
. . . . . . . . 9
⊢
({A, B} = 〈x,
y〉 ↔ ((A = {x} ∧ B = {x, y}) ∨ (A = {x, y} ∧ B = {x}))) |
54 | | idd 21 |
. . . . . . . . . 10
⊢ (A = {w} →
((A = {x} ∧ B = {x, y}) → (A =
{x} ∧
B = {x,
y}))) |
55 | | eqtr2 2055 |
. . . . . . . . . . . . . 14
⊢
((A = {x, y} ∧ A = {w}) → {x,
y} = {w}) |
56 | | vex 2554 |
. . . . . . . . . . . . . . . 16
⊢ w ∈
V |
57 | 20, 21, 56 | preqsn 3537 |
. . . . . . . . . . . . . . 15
⊢
({x, y} = {w} ↔
(x = y
∧ y =
w)) |
58 | 57 | simplbi 259 |
. . . . . . . . . . . . . 14
⊢
({x, y} = {w} →
x = y) |
59 | 55, 58 | syl 14 |
. . . . . . . . . . . . 13
⊢
((A = {x, y} ∧ A = {w}) → x =
y) |
60 | | dfsn2 3381 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {x} = {x,
x} |
61 | | preq2 3439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (x = y →
{x, x}
= {x, y}) |
62 | 60, 61 | syl5req 2082 |
. . . . . . . . . . . . . . . . . . 19
⊢ (x = y →
{x, y}
= {x}) |
63 | 62 | eqeq2d 2048 |
. . . . . . . . . . . . . . . . . 18
⊢ (x = y →
(A = {x, y} ↔
A = {x})) |
64 | 60, 61 | syl5eq 2081 |
. . . . . . . . . . . . . . . . . . 19
⊢ (x = y →
{x} = {x, y}) |
65 | 64 | eqeq2d 2048 |
. . . . . . . . . . . . . . . . . 18
⊢ (x = y →
(B = {x} ↔ B =
{x, y})) |
66 | 63, 65 | anbi12d 442 |
. . . . . . . . . . . . . . . . 17
⊢ (x = y →
((A = {x, y} ∧ B = {x}) ↔ (A =
{x} ∧
B = {x,
y}))) |
67 | 66 | biimpd 132 |
. . . . . . . . . . . . . . . 16
⊢ (x = y →
((A = {x, y} ∧ B = {x}) → (A =
{x} ∧
B = {x,
y}))) |
68 | 67 | expd 245 |
. . . . . . . . . . . . . . 15
⊢ (x = y →
(A = {x, y} →
(B = {x} → (A =
{x} ∧
B = {x,
y})))) |
69 | 68 | com12 27 |
. . . . . . . . . . . . . 14
⊢ (A = {x, y} → (x =
y → (B = {x} →
(A = {x} ∧ B = {x, y})))) |
70 | 69 | adantr 261 |
. . . . . . . . . . . . 13
⊢
((A = {x, y} ∧ A = {w}) → (x =
y → (B = {x} →
(A = {x} ∧ B = {x, y})))) |
71 | 59, 70 | mpd 13 |
. . . . . . . . . . . 12
⊢
((A = {x, y} ∧ A = {w}) → (B =
{x} → (A = {x} ∧ B = {x, y}))) |
72 | 71 | expcom 109 |
. . . . . . . . . . 11
⊢ (A = {w} →
(A = {x, y} →
(B = {x} → (A =
{x} ∧
B = {x,
y})))) |
73 | 72 | impd 242 |
. . . . . . . . . 10
⊢ (A = {w} →
((A = {x, y} ∧ B = {x}) → (A =
{x} ∧
B = {x,
y}))) |
74 | 54, 73 | jaod 636 |
. . . . . . . . 9
⊢ (A = {w} →
(((A = {x} ∧ B = {x, y}) ∨ (A = {x, y} ∧ B = {x})) →
(A = {x} ∧ B = {x, y}))) |
75 | 53, 74 | syl5bi 141 |
. . . . . . . 8
⊢ (A = {w} →
({A, B}
= 〈x, y〉 → (A = {x} ∧ B = {x, y}))) |
76 | 75 | 2eximdv 1759 |
. . . . . . 7
⊢ (A = {w} →
(∃x∃y{A, B} =
〈x, y〉 → ∃x∃y(A = {x} ∧ B = {x, y}))) |
77 | 76 | exlimiv 1486 |
. . . . . 6
⊢ (∃w A = {w} →
(∃x∃y{A, B} =
〈x, y〉 → ∃x∃y(A = {x} ∧ B = {x, y}))) |
78 | 77 | imp 115 |
. . . . 5
⊢ ((∃w A = {w} ∧ ∃x∃y{A, B} = 〈x,
y〉) → ∃x∃y(A = {x} ∧ B = {x, y})) |
79 | 41, 50, 78 | syl2an 273 |
. . . 4
⊢ ((∀z(z = {A} →
∃x∃y z = 〈x,
y〉) ∧
∀z(z = {A, B} →
∃x∃y z = 〈x,
y〉)) → ∃x∃y(A = {x} ∧ B = {x, y})) |
80 | 14, 79 | sylbi 114 |
. . 3
⊢
(〈A, B〉 ⊆ (V × V) → ∃x∃y(A = {x} ∧ B = {x, y})) |
81 | | simpr 103 |
. . . . . . . . . . 11
⊢
((A = {x} ∧ z = {A}) →
z = {A}) |
82 | | equid 1586 |
. . . . . . . . . . . . . 14
⊢ x = x |
83 | 82 | jctl 297 |
. . . . . . . . . . . . 13
⊢ (A = {x} →
(x = x
∧ A =
{x})) |
84 | 20, 20, 4 | opeqsn 3980 |
. . . . . . . . . . . . 13
⊢
(〈x, x〉 = {A}
↔ (x = x ∧ A = {x})) |
85 | 83, 84 | sylibr 137 |
. . . . . . . . . . . 12
⊢ (A = {x} →
〈x, x〉 = {A}) |
86 | 85 | adantr 261 |
. . . . . . . . . . 11
⊢
((A = {x} ∧ z = {A}) →
〈x, x〉 = {A}) |
87 | 81, 86 | eqtr4d 2072 |
. . . . . . . . . 10
⊢
((A = {x} ∧ z = {A}) →
z = 〈x, x〉) |
88 | | opeq12 3542 |
. . . . . . . . . . . 12
⊢
((w = x ∧ v = x) →
〈w, v〉 = 〈x, x〉) |
89 | 88 | eqeq2d 2048 |
. . . . . . . . . . 11
⊢
((w = x ∧ v = x) →
(z = 〈w, v〉
↔ z = 〈x, x〉)) |
90 | 20, 20, 89 | spc2ev 2642 |
. . . . . . . . . 10
⊢ (z = 〈x,
x〉 → ∃w∃v z = 〈w,
v〉) |
91 | 87, 90 | syl 14 |
. . . . . . . . 9
⊢
((A = {x} ∧ z = {A}) →
∃w∃v z = 〈w,
v〉) |
92 | 91 | adantlr 446 |
. . . . . . . 8
⊢
(((A = {x} ∧ B = {x, y}) ∧ z = {A}) →
∃w∃v z = 〈w,
v〉) |
93 | | preq12 3440 |
. . . . . . . . . . . 12
⊢
((A = {x} ∧ B = {x, y}) → {A,
B} = {{x}, {x, y}}) |
94 | 93 | eqeq2d 2048 |
. . . . . . . . . . 11
⊢
((A = {x} ∧ B = {x, y}) → (z =
{A, B}
↔ z = {{x}, {x, y}})) |
95 | 94 | biimpa 280 |
. . . . . . . . . 10
⊢
(((A = {x} ∧ B = {x, y}) ∧ z = {A, B}) → z =
{{x}, {x, y}}) |
96 | 20, 21 | dfop 3539 |
. . . . . . . . . 10
⊢
〈x, y〉 = {{x},
{x, y}} |
97 | 95, 96 | syl6eqr 2087 |
. . . . . . . . 9
⊢
(((A = {x} ∧ B = {x, y}) ∧ z = {A, B}) → z =
〈x, y〉) |
98 | | opeq12 3542 |
. . . . . . . . . . 11
⊢
((w = x ∧ v = y) →
〈w, v〉 = 〈x, y〉) |
99 | 98 | eqeq2d 2048 |
. . . . . . . . . 10
⊢
((w = x ∧ v = y) →
(z = 〈w, v〉
↔ z = 〈x, y〉)) |
100 | 20, 21, 99 | spc2ev 2642 |
. . . . . . . . 9
⊢ (z = 〈x,
y〉 → ∃w∃v z = 〈w,
v〉) |
101 | 97, 100 | syl 14 |
. . . . . . . 8
⊢
(((A = {x} ∧ B = {x, y}) ∧ z = {A, B}) → ∃w∃v z = 〈w,
v〉) |
102 | 92, 101 | jaodan 709 |
. . . . . . 7
⊢
(((A = {x} ∧ B = {x, y}) ∧ (z = {A} ∨ z = {A, B})) →
∃w∃v z = 〈w,
v〉) |
103 | 102 | ex 108 |
. . . . . 6
⊢
((A = {x} ∧ B = {x, y}) → ((z =
{A} ∨
z = {A,
B}) → ∃w∃v z = 〈w,
v〉)) |
104 | | elvv 4345 |
. . . . . 6
⊢ (z ∈ (V × V)
↔ ∃w∃v z =
〈w, v〉) |
105 | 103, 6, 104 | 3imtr4g 194 |
. . . . 5
⊢
((A = {x} ∧ B = {x, y}) → (z
∈ 〈A, B〉
→ z ∈ (V × V))) |
106 | 105 | ssrdv 2945 |
. . . 4
⊢
((A = {x} ∧ B = {x, y}) → 〈A, B〉
⊆ (V × V)) |
107 | 106 | exlimivv 1773 |
. . 3
⊢ (∃x∃y(A = {x} ∧ B = {x, y}) →
〈A, B〉 ⊆ (V × V)) |
108 | 80, 107 | impbii 117 |
. 2
⊢
(〈A, B〉 ⊆ (V × V) ↔ ∃x∃y(A = {x} ∧ B = {x, y})) |
109 | 1, 108 | bitri 173 |
1
⊢ (Rel
〈A, B〉 ↔ ∃x∃y(A = {x} ∧ B = {x, y})) |