Step |
Hyp |
Ref |
Expression |
1 |
|
dfac5lem.1 |
⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } |
2 |
1
|
unieqi |
⊢ ∪ 𝐴 = ∪ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } |
3 |
2
|
eleq2i |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ ∪ 𝐴 ↔ 〈 𝑤 , 𝑔 〉 ∈ ∪ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ) |
4 |
|
eluniab |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ ∪ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ↔ ∃ 𝑢 ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ) |
5 |
|
r19.42v |
⊢ ( ∃ 𝑡 ∈ ℎ ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) |
6 |
|
anass |
⊢ ( ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ) |
7 |
5 6
|
bitr2i |
⊢ ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ↔ ∃ 𝑡 ∈ ℎ ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) |
8 |
7
|
exbii |
⊢ ( ∃ 𝑢 ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ↔ ∃ 𝑢 ∃ 𝑡 ∈ ℎ ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) |
9 |
|
rexcom4 |
⊢ ( ∃ 𝑡 ∈ ℎ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ∃ 𝑢 ∃ 𝑡 ∈ ℎ ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) |
10 |
|
df-rex |
⊢ ( ∃ 𝑡 ∈ ℎ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ∃ 𝑡 ( 𝑡 ∈ ℎ ∧ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ) |
11 |
9 10
|
bitr3i |
⊢ ( ∃ 𝑢 ∃ 𝑡 ∈ ℎ ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ∃ 𝑡 ( 𝑡 ∈ ℎ ∧ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ) |
12 |
4 8 11
|
3bitri |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ ∪ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ↔ ∃ 𝑡 ( 𝑡 ∈ ℎ ∧ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ) |
13 |
|
ancom |
⊢ ( ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑢 = ( { 𝑡 } × 𝑡 ) ∧ ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ) ) |
14 |
|
ne0i |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 → 𝑢 ≠ ∅ ) |
15 |
14
|
pm4.71i |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ↔ ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ) |
16 |
15
|
anbi2i |
⊢ ( ( 𝑢 = ( { 𝑡 } × 𝑡 ) ∧ 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ) ↔ ( 𝑢 = ( { 𝑡 } × 𝑡 ) ∧ ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ) ) |
17 |
13 16
|
bitr4i |
⊢ ( ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑢 = ( { 𝑡 } × 𝑡 ) ∧ 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ) ) |
18 |
17
|
exbii |
⊢ ( ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ∃ 𝑢 ( 𝑢 = ( { 𝑡 } × 𝑡 ) ∧ 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ) ) |
19 |
|
snex |
⊢ { 𝑡 } ∈ V |
20 |
|
vex |
⊢ 𝑡 ∈ V |
21 |
19 20
|
xpex |
⊢ ( { 𝑡 } × 𝑡 ) ∈ V |
22 |
|
eleq2 |
⊢ ( 𝑢 = ( { 𝑡 } × 𝑡 ) → ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ↔ 〈 𝑤 , 𝑔 〉 ∈ ( { 𝑡 } × 𝑡 ) ) ) |
23 |
21 22
|
ceqsexv |
⊢ ( ∃ 𝑢 ( 𝑢 = ( { 𝑡 } × 𝑡 ) ∧ 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ) ↔ 〈 𝑤 , 𝑔 〉 ∈ ( { 𝑡 } × 𝑡 ) ) |
24 |
18 23
|
bitri |
⊢ ( ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ 〈 𝑤 , 𝑔 〉 ∈ ( { 𝑡 } × 𝑡 ) ) |
25 |
24
|
anbi2i |
⊢ ( ( 𝑡 ∈ ℎ ∧ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ↔ ( 𝑡 ∈ ℎ ∧ 〈 𝑤 , 𝑔 〉 ∈ ( { 𝑡 } × 𝑡 ) ) ) |
26 |
|
opelxp |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ ( { 𝑡 } × 𝑡 ) ↔ ( 𝑤 ∈ { 𝑡 } ∧ 𝑔 ∈ 𝑡 ) ) |
27 |
|
velsn |
⊢ ( 𝑤 ∈ { 𝑡 } ↔ 𝑤 = 𝑡 ) |
28 |
|
equcom |
⊢ ( 𝑤 = 𝑡 ↔ 𝑡 = 𝑤 ) |
29 |
27 28
|
bitri |
⊢ ( 𝑤 ∈ { 𝑡 } ↔ 𝑡 = 𝑤 ) |
30 |
29
|
anbi1i |
⊢ ( ( 𝑤 ∈ { 𝑡 } ∧ 𝑔 ∈ 𝑡 ) ↔ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡 ) ) |
31 |
26 30
|
bitri |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ ( { 𝑡 } × 𝑡 ) ↔ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡 ) ) |
32 |
31
|
anbi2i |
⊢ ( ( 𝑡 ∈ ℎ ∧ 〈 𝑤 , 𝑔 〉 ∈ ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑡 ∈ ℎ ∧ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡 ) ) ) |
33 |
|
an12 |
⊢ ( ( 𝑡 ∈ ℎ ∧ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡 ) ) ↔ ( 𝑡 = 𝑤 ∧ ( 𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡 ) ) ) |
34 |
25 32 33
|
3bitri |
⊢ ( ( 𝑡 ∈ ℎ ∧ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ↔ ( 𝑡 = 𝑤 ∧ ( 𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡 ) ) ) |
35 |
34
|
exbii |
⊢ ( ∃ 𝑡 ( 𝑡 ∈ ℎ ∧ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ↔ ∃ 𝑡 ( 𝑡 = 𝑤 ∧ ( 𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡 ) ) ) |
36 |
|
vex |
⊢ 𝑤 ∈ V |
37 |
|
elequ1 |
⊢ ( 𝑡 = 𝑤 → ( 𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ ) ) |
38 |
|
eleq2 |
⊢ ( 𝑡 = 𝑤 → ( 𝑔 ∈ 𝑡 ↔ 𝑔 ∈ 𝑤 ) ) |
39 |
37 38
|
anbi12d |
⊢ ( 𝑡 = 𝑤 → ( ( 𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡 ) ↔ ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) ) ) |
40 |
36 39
|
ceqsexv |
⊢ ( ∃ 𝑡 ( 𝑡 = 𝑤 ∧ ( 𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡 ) ) ↔ ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) ) |
41 |
35 40
|
bitri |
⊢ ( ∃ 𝑡 ( 𝑡 ∈ ℎ ∧ ∃ 𝑢 ( ( 〈 𝑤 , 𝑔 〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅ ) ∧ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ) ↔ ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) ) |
42 |
3 12 41
|
3bitri |
⊢ ( 〈 𝑤 , 𝑔 〉 ∈ ∪ 𝐴 ↔ ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) ) |