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

Metamath Proof Explorer

Theorem dfac5lem2

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

Ref Expression
Hypothesis dfac5lem.1 ⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
Assertion dfac5lem2 ( ⟨ 𝑤 , 𝑔 ⟩ ∈ ∪ 𝐴 ↔ ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) )

Proof

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 vsnex ⊢ { 𝑡 } ∈ 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 ⊢ ( ⟨ 𝑤 , 𝑔 ⟩ ∈ ∪ 𝐴 ↔ ( 𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤 ) )