Metamath Proof Explorer


Theorem dfac5lem3

Description: Lemma for dfac5 . (Contributed by NM, 12-Apr-2004)

Ref Expression
Hypothesis dfac5lem.1 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
Assertion dfac5lem3 ( ( { 𝑤 } × 𝑤 ) ∈ 𝐴 ↔ ( 𝑤 ≠ ∅ ∧ 𝑤 ) )

Proof

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 ( ( { 𝑤 } × 𝑤 ) ∈ 𝐴 ↔ ( 𝑤 ≠ ∅ ∧ 𝑤 ) )