This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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