Theorem dfac5lem1

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

	Ref	Expression
Assertion	dfac5lem1	⊢ ( ∃! 𝑣 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ↔ ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ↔ ( 𝑣 ∈ ( { 𝑤 } × 𝑤 ) ∧ 𝑣 ∈ 𝑦 ) )
2		elxp	⊢ ( 𝑣 ∈ ( { 𝑤 } × 𝑤 ) ↔ ∃ 𝑡 ∃ 𝑔 ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) )
3		excom	⊢ ( ∃ 𝑡 ∃ 𝑔 ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ↔ ∃ 𝑔 ∃ 𝑡 ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) )
4	2 3	bitri	⊢ ( 𝑣 ∈ ( { 𝑤 } × 𝑤 ) ↔ ∃ 𝑔 ∃ 𝑡 ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) )
5	4	anbi1i	⊢ ( ( 𝑣 ∈ ( { 𝑤 } × 𝑤 ) ∧ 𝑣 ∈ 𝑦 ) ↔ ( ∃ 𝑔 ∃ 𝑡 ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) )
6		19.41vv	⊢ ( ∃ 𝑔 ∃ 𝑡 ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) ↔ ( ∃ 𝑔 ∃ 𝑡 ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) )
7		an32	⊢ ( ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) ↔ ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ 𝑣 ∈ 𝑦 ) ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) )
8		eleq1	⊢ ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ → ( 𝑣 ∈ 𝑦 ↔ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) )
9	8	pm5.32i	⊢ ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ 𝑣 ∈ 𝑦 ) ↔ ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) )
10		velsn	⊢ ( 𝑡 ∈ { 𝑤 } ↔ 𝑡 = 𝑤 )
11	10	anbi1i	⊢ ( ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ↔ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤 ) )
12	9 11	anbi12i	⊢ ( ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ 𝑣 ∈ 𝑦 ) ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ↔ ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ∧ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤 ) ) )
13		an4	⊢ ( ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ∧ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤 ) ) ↔ ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ 𝑡 = 𝑤 ) ∧ ( ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ∧ 𝑔 ∈ 𝑤 ) ) )
14		ancom	⊢ ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ 𝑡 = 𝑤 ) ↔ ( 𝑡 = 𝑤 ∧ 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ) )
15		ancom	⊢ ( ( ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ∧ 𝑔 ∈ 𝑤 ) ↔ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) )
16	14 15	anbi12i	⊢ ( ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ 𝑡 = 𝑤 ) ∧ ( ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ∧ 𝑔 ∈ 𝑤 ) ) ↔ ( ( 𝑡 = 𝑤 ∧ 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ) ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) )
17		anass	⊢ ( ( ( 𝑡 = 𝑤 ∧ 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ) ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) ↔ ( 𝑡 = 𝑤 ∧ ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) ) )
18	13 16 17	3bitri	⊢ ( ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ∧ ( 𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑤 ) ) ↔ ( 𝑡 = 𝑤 ∧ ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) ) )
19	7 12 18	3bitri	⊢ ( ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) ↔ ( 𝑡 = 𝑤 ∧ ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) ) )
20	19	exbii	⊢ ( ∃ 𝑡 ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) ↔ ∃ 𝑡 ( 𝑡 = 𝑤 ∧ ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) ) )
21		opeq1	⊢ ( 𝑡 = 𝑤 → ⟨ 𝑡 , 𝑔 ⟩ = ⟨ 𝑤 , 𝑔 ⟩ )
22	21	eqeq2d	⊢ ( 𝑡 = 𝑤 → ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ↔ 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ) )
23	21	eleq1d	⊢ ( 𝑡 = 𝑤 → ( ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ↔ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )
24	23	anbi2d	⊢ ( 𝑡 = 𝑤 → ( ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ↔ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
25	22 24	anbi12d	⊢ ( 𝑡 = 𝑤 → ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) ↔ ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) ) )
26	25	equsexvw	⊢ ( ∃ 𝑡 ( 𝑡 = 𝑤 ∧ ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑡 , 𝑔 ⟩ ∈ 𝑦 ) ) ) ↔ ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
27	20 26	bitri	⊢ ( ∃ 𝑡 ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) ↔ ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
28	27	exbii	⊢ ( ∃ 𝑔 ∃ 𝑡 ( ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) ↔ ∃ 𝑔 ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
29	6 28	bitr3i	⊢ ( ( ∃ 𝑔 ∃ 𝑡 ( 𝑣 = ⟨ 𝑡 , 𝑔 ⟩ ∧ ( 𝑡 ∈ { 𝑤 } ∧ 𝑔 ∈ 𝑤 ) ) ∧ 𝑣 ∈ 𝑦 ) ↔ ∃ 𝑔 ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
30	1 5 29	3bitri	⊢ ( 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ↔ ∃ 𝑔 ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
31	30	eubii	⊢ ( ∃! 𝑣 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ↔ ∃! 𝑣 ∃ 𝑔 ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) )
32		vex	⊢ 𝑤 ∈ V
33	32	euop2	⊢ ( ∃! 𝑣 ∃ 𝑔 ( 𝑣 = ⟨ 𝑤 , 𝑔 ⟩ ∧ ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) ) ↔ ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )
34	31 33	bitri	⊢ ( ∃! 𝑣 𝑣 ∈ ( ( { 𝑤 } × 𝑤 ) ∩ 𝑦 ) ↔ ∃! 𝑔 ( 𝑔 ∈ 𝑤 ∧ ⟨ 𝑤 , 𝑔 ⟩ ∈ 𝑦 ) )