Theorem dfac5lem4OLD

Description: Obsolete version of dfac5lem4 as of 23-Jun-2025. (Contributed by NM, 11-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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