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