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