Theorem dfac5lem4

Description: Lemma for dfac5 . (Contributed by NM, 11-Apr-2004) Avoid ax-11 . (Revised by BTernaryTau, 23-Jun-2025)

	Ref	Expression
Hypotheses	dfac5lem.1	⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
	dfac5lem.2	⊢ ( 𝜑 ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
Assertion	dfac5lem4	⊢ ( 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		dfac5lem.1	⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
2		dfac5lem.2	⊢ ( 𝜑 ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
3		vex	⊢ 𝑧 ∈ V
4		neeq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅ ) )
5		eqeq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
6	5	rexbidv	⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
7	4 6	anbi12d	⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑧 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) ) )
8	3 7	elab	⊢ ( 𝑧 ∈ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ↔ ( 𝑧 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
9	8	simplbi	⊢ ( 𝑧 ∈ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } → 𝑧 ≠ ∅ )
10	9 1	eleq2s	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ≠ ∅ )
11	10	rgen	⊢ ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅
12		df-an	⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) ↔ ¬ ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) )
13	3 7 1	elab2	⊢ ( 𝑧 ∈ 𝐴 ↔ ( 𝑧 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
14	13	simprbi	⊢ ( 𝑧 ∈ 𝐴 → ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) )
15		vex	⊢ 𝑤 ∈ V
16		neeq1	⊢ ( 𝑢 = 𝑤 → ( 𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅ ) )
17		eqeq1	⊢ ( 𝑢 = 𝑤 → ( 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ 𝑤 = ( { 𝑡 } × 𝑡 ) ) )
18	17	rexbidv	⊢ ( 𝑢 = 𝑤 → ( ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ) )
19	16 18	anbi12d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ) ) )
20	15 19 1	elab2	⊢ ( 𝑤 ∈ 𝐴 ↔ ( 𝑤 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ) )
21	20	simprbi	⊢ ( 𝑤 ∈ 𝐴 → ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) )
22		sneq	⊢ ( 𝑡 = 𝑔 → { 𝑡 } = { 𝑔 } )
23	22	xpeq1d	⊢ ( 𝑡 = 𝑔 → ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑡 ) )
24		xpeq2	⊢ ( 𝑡 = 𝑔 → ( { 𝑔 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) )
25	23 24	eqtrd	⊢ ( 𝑡 = 𝑔 → ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) )
26	25	eqeq2d	⊢ ( 𝑡 = 𝑔 → ( 𝑤 = ( { 𝑡 } × 𝑡 ) ↔ 𝑤 = ( { 𝑔 } × 𝑔 ) ) )
27	26	cbvrexvw	⊢ ( ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) )
28	21 27	sylib	⊢ ( 𝑤 ∈ 𝐴 → ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) )
29		eleq2	⊢ ( 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( { 𝑡 } × 𝑡 ) ) )
30		elxp	⊢ ( 𝑥 ∈ ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑢 ∃ 𝑣 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
31		opeq1	⊢ ( 𝑢 = 𝑠 → ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑠 , 𝑣 ⟩ )
32	31	eqeq2d	⊢ ( 𝑢 = 𝑠 → ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ↔ 𝑥 = ⟨ 𝑠 , 𝑣 ⟩ ) )
33		eleq1w	⊢ ( 𝑢 = 𝑠 → ( 𝑢 ∈ { 𝑡 } ↔ 𝑠 ∈ { 𝑡 } ) )
34	33	anbi1d	⊢ ( 𝑢 = 𝑠 → ( ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ↔ ( 𝑠 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
35	32 34	anbi12d	⊢ ( 𝑢 = 𝑠 → ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ↔ ( 𝑥 = ⟨ 𝑠 , 𝑣 ⟩ ∧ ( 𝑠 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ) )
36	35	excomimw	⊢ ( ∃ 𝑢 ∃ 𝑣 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) → ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
37	30 36	sylbi	⊢ ( 𝑥 ∈ ( { 𝑡 } × 𝑡 ) → ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
38	29 37	biimtrdi	⊢ ( 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ) )
39		eleq2	⊢ ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ( { 𝑔 } × 𝑔 ) ) )
40		elxp	⊢ ( 𝑥 ∈ ( { 𝑔 } × 𝑔 ) ↔ ∃ 𝑢 ∃ 𝑦 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
41		opeq1	⊢ ( 𝑢 = 𝑠 → ⟨ 𝑢 , 𝑦 ⟩ = ⟨ 𝑠 , 𝑦 ⟩ )
42	41	eqeq2d	⊢ ( 𝑢 = 𝑠 → ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ↔ 𝑥 = ⟨ 𝑠 , 𝑦 ⟩ ) )
43		eleq1w	⊢ ( 𝑢 = 𝑠 → ( 𝑢 ∈ { 𝑔 } ↔ 𝑠 ∈ { 𝑔 } ) )
44	43	anbi1d	⊢ ( 𝑢 = 𝑠 → ( ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ↔ ( 𝑠 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
45	42 44	anbi12d	⊢ ( 𝑢 = 𝑠 → ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ↔ ( 𝑥 = ⟨ 𝑠 , 𝑦 ⟩ ∧ ( 𝑠 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) )
46	45	excomimw	⊢ ( ∃ 𝑢 ∃ 𝑦 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) → ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
47	40 46	sylbi	⊢ ( 𝑥 ∈ ( { 𝑔 } × 𝑔 ) → ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
48	39 47	biimtrdi	⊢ ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( 𝑥 ∈ 𝑤 → ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) )
49	38 48	im2anan9	⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → ( ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) ) )
50		exdistrv	⊢ ( ∃ 𝑣 ∃ 𝑦 ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) ↔ ( ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) )
51	49 50	imbitrrdi	⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → ∃ 𝑣 ∃ 𝑦 ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) ) )
52		velsn	⊢ ( 𝑢 ∈ { 𝑡 } ↔ 𝑢 = 𝑡 )
53		opeq1	⊢ ( 𝑢 = 𝑡 → ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑡 , 𝑣 ⟩ )
54	53	eqeq2d	⊢ ( 𝑢 = 𝑡 → ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ↔ 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ ) )
55	54	biimpac	⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ 𝑢 = 𝑡 ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
56	52 55	sylan2b	⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ 𝑢 ∈ { 𝑡 } ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
57	56	adantrr	⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
58	57	exlimiv	⊢ ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
59		velsn	⊢ ( 𝑢 ∈ { 𝑔 } ↔ 𝑢 = 𝑔 )
60		opeq1	⊢ ( 𝑢 = 𝑔 → ⟨ 𝑢 , 𝑦 ⟩ = ⟨ 𝑔 , 𝑦 ⟩ )
61	60	eqeq2d	⊢ ( 𝑢 = 𝑔 → ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ↔ 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ ) )
62	61	biimpac	⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ 𝑢 = 𝑔 ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
63	59 62	sylan2b	⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ 𝑢 ∈ { 𝑔 } ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
64	63	adantrr	⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
65	64	exlimiv	⊢ ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
66	58 65	sylan9req	⊢ ( ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) → ⟨ 𝑡 , 𝑣 ⟩ = ⟨ 𝑔 , 𝑦 ⟩ )
67		vex	⊢ 𝑡 ∈ V
68		vex	⊢ 𝑣 ∈ V
69	67 68	opth1	⊢ ( ⟨ 𝑡 , 𝑣 ⟩ = ⟨ 𝑔 , 𝑦 ⟩ → 𝑡 = 𝑔 )
70	66 69	syl	⊢ ( ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) → 𝑡 = 𝑔 )
71	70	exlimivv	⊢ ( ∃ 𝑣 ∃ 𝑦 ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) → 𝑡 = 𝑔 )
72	51 71	syl6	⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑡 = 𝑔 ) )
73	72 25	syl6	⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) ) )
74		eqeq12	⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( 𝑧 = 𝑤 ↔ ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) ) )
75	73 74	sylibrd	⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
76	75	ex	⊢ ( 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) ) )
77	76	rexlimivw	⊢ ( ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) ) )
78	77	rexlimdvw	⊢ ( ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) → ( ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) ) )
79	78	imp	⊢ ( ( ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
80	14 28 79	syl2an	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
81	12 80	biimtrrid	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
82	81	necon1ad	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) ) )
83	82	alrimdv	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) ) )
84		disj1	⊢ ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) )
85	83 84	imbitrrdi	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
86	85	rgen2	⊢ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ )
87		vex	⊢ ℎ ∈ V
88		vuniex	⊢ ∪ ℎ ∈ V
89	87 88	xpex	⊢ ( ℎ × ∪ ℎ ) ∈ V
90	89	pwex	⊢ 𝒫 ( ℎ × ∪ ℎ ) ∈ V
91		snssi	⊢ ( 𝑡 ∈ ℎ → { 𝑡 } ⊆ ℎ )
92		elssuni	⊢ ( 𝑡 ∈ ℎ → 𝑡 ⊆ ∪ ℎ )
93		xpss12	⊢ ( ( { 𝑡 } ⊆ ℎ ∧ 𝑡 ⊆ ∪ ℎ ) → ( { 𝑡 } × 𝑡 ) ⊆ ( ℎ × ∪ ℎ ) )
94	91 92 93	syl2anc	⊢ ( 𝑡 ∈ ℎ → ( { 𝑡 } × 𝑡 ) ⊆ ( ℎ × ∪ ℎ ) )
95		vsnex	⊢ { 𝑡 } ∈ V
96	95 67	xpex	⊢ ( { 𝑡 } × 𝑡 ) ∈ V
97	96	elpw	⊢ ( ( { 𝑡 } × 𝑡 ) ∈ 𝒫 ( ℎ × ∪ ℎ ) ↔ ( { 𝑡 } × 𝑡 ) ⊆ ( ℎ × ∪ ℎ ) )
98	94 97	sylibr	⊢ ( 𝑡 ∈ ℎ → ( { 𝑡 } × 𝑡 ) ∈ 𝒫 ( ℎ × ∪ ℎ ) )
99		eleq1	⊢ ( 𝑢 = ( { 𝑡 } × 𝑡 ) → ( 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) ↔ ( { 𝑡 } × 𝑡 ) ∈ 𝒫 ( ℎ × ∪ ℎ ) ) )
100	98 99	syl5ibrcom	⊢ ( 𝑡 ∈ ℎ → ( 𝑢 = ( { 𝑡 } × 𝑡 ) → 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) ) )
101	100	rexlimiv	⊢ ( ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) → 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) )
102	101	adantl	⊢ ( ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) → 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) )
103	102	abssi	⊢ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ⊆ 𝒫 ( ℎ × ∪ ℎ )
104	90 103	ssexi	⊢ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ∈ V
105	1 104	eqeltri	⊢ 𝐴 ∈ V
106		raleq	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ) )
107		raleq	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
108	107	raleqbi1dv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
109	106 108	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ↔ ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) )
110		raleq	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
111	110	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
112	109 111	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
113	105 112	spcv	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ( ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
114	2 113	sylbi	⊢ ( 𝜑 → ( ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
115	11 86 114	mp2ani	⊢ ( 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )