Step |
Hyp |
Ref |
Expression |
1 |
|
dfac5lem.1 |
⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } |
2 |
|
snex |
⊢ { 𝑤 } ∈ V |
3 |
|
vex |
⊢ 𝑤 ∈ V |
4 |
2 3
|
xpex |
⊢ ( { 𝑤 } × 𝑤 ) ∈ V |
5 |
|
neeq1 |
⊢ ( 𝑢 = ( { 𝑤 } × 𝑤 ) → ( 𝑢 ≠ ∅ ↔ ( { 𝑤 } × 𝑤 ) ≠ ∅ ) ) |
6 |
|
eqeq1 |
⊢ ( 𝑢 = ( { 𝑤 } × 𝑤 ) → ( 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑢 = ( { 𝑤 } × 𝑤 ) → ( ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑡 ∈ ℎ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ) |
8 |
5 7
|
anbi12d |
⊢ ( 𝑢 = ( { 𝑤 } × 𝑤 ) → ( ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( ( { 𝑤 } × 𝑤 ) ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ) ) |
9 |
4 8
|
elab |
⊢ ( ( { 𝑤 } × 𝑤 ) ∈ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ↔ ( ( { 𝑤 } × 𝑤 ) ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ) |
10 |
1
|
eleq2i |
⊢ ( ( { 𝑤 } × 𝑤 ) ∈ 𝐴 ↔ ( { 𝑤 } × 𝑤 ) ∈ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ) |
11 |
|
xpeq2 |
⊢ ( 𝑤 = ∅ → ( { 𝑤 } × 𝑤 ) = ( { 𝑤 } × ∅ ) ) |
12 |
|
xp0 |
⊢ ( { 𝑤 } × ∅ ) = ∅ |
13 |
11 12
|
eqtrdi |
⊢ ( 𝑤 = ∅ → ( { 𝑤 } × 𝑤 ) = ∅ ) |
14 |
|
rneq |
⊢ ( ( { 𝑤 } × 𝑤 ) = ∅ → ran ( { 𝑤 } × 𝑤 ) = ran ∅ ) |
15 |
3
|
snnz |
⊢ { 𝑤 } ≠ ∅ |
16 |
|
rnxp |
⊢ ( { 𝑤 } ≠ ∅ → ran ( { 𝑤 } × 𝑤 ) = 𝑤 ) |
17 |
15 16
|
ax-mp |
⊢ ran ( { 𝑤 } × 𝑤 ) = 𝑤 |
18 |
|
rn0 |
⊢ ran ∅ = ∅ |
19 |
14 17 18
|
3eqtr3g |
⊢ ( ( { 𝑤 } × 𝑤 ) = ∅ → 𝑤 = ∅ ) |
20 |
13 19
|
impbii |
⊢ ( 𝑤 = ∅ ↔ ( { 𝑤 } × 𝑤 ) = ∅ ) |
21 |
20
|
necon3bii |
⊢ ( 𝑤 ≠ ∅ ↔ ( { 𝑤 } × 𝑤 ) ≠ ∅ ) |
22 |
|
df-rex |
⊢ ( ∃ 𝑡 ∈ ℎ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑡 ( 𝑡 ∈ ℎ ∧ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ) |
23 |
|
rneq |
⊢ ( ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) → ran ( { 𝑤 } × 𝑤 ) = ran ( { 𝑡 } × 𝑡 ) ) |
24 |
|
vex |
⊢ 𝑡 ∈ V |
25 |
24
|
snnz |
⊢ { 𝑡 } ≠ ∅ |
26 |
|
rnxp |
⊢ ( { 𝑡 } ≠ ∅ → ran ( { 𝑡 } × 𝑡 ) = 𝑡 ) |
27 |
25 26
|
ax-mp |
⊢ ran ( { 𝑡 } × 𝑡 ) = 𝑡 |
28 |
23 17 27
|
3eqtr3g |
⊢ ( ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) → 𝑤 = 𝑡 ) |
29 |
|
sneq |
⊢ ( 𝑤 = 𝑡 → { 𝑤 } = { 𝑡 } ) |
30 |
29
|
xpeq1d |
⊢ ( 𝑤 = 𝑡 → ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑤 ) ) |
31 |
|
xpeq2 |
⊢ ( 𝑤 = 𝑡 → ( { 𝑡 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) |
32 |
30 31
|
eqtrd |
⊢ ( 𝑤 = 𝑡 → ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) |
33 |
28 32
|
impbii |
⊢ ( ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ↔ 𝑤 = 𝑡 ) |
34 |
|
equcom |
⊢ ( 𝑤 = 𝑡 ↔ 𝑡 = 𝑤 ) |
35 |
33 34
|
bitri |
⊢ ( ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ↔ 𝑡 = 𝑤 ) |
36 |
35
|
anbi1ci |
⊢ ( ( 𝑡 ∈ ℎ ∧ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ ) ) |
37 |
36
|
exbii |
⊢ ( ∃ 𝑡 ( 𝑡 ∈ ℎ ∧ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ↔ ∃ 𝑡 ( 𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ ) ) |
38 |
|
elequ1 |
⊢ ( 𝑡 = 𝑤 → ( 𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ ) ) |
39 |
38
|
equsexvw |
⊢ ( ∃ 𝑡 ( 𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ ) ↔ 𝑤 ∈ ℎ ) |
40 |
22 37 39
|
3bitrri |
⊢ ( 𝑤 ∈ ℎ ↔ ∃ 𝑡 ∈ ℎ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) |
41 |
21 40
|
anbi12i |
⊢ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) ↔ ( ( { 𝑤 } × 𝑤 ) ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ ( { 𝑤 } × 𝑤 ) = ( { 𝑡 } × 𝑡 ) ) ) |
42 |
9 10 41
|
3bitr4i |
⊢ ( ( { 𝑤 } × 𝑤 ) ∈ 𝐴 ↔ ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ ) ) |