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 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 ( ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝐴 ↔ ( 𝑤𝑔𝑤 ) )