Theorem dfac5lem4 10130

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

Hypotheses

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

Assertion

Ref	Expression
dfac5lem4	⊢ (𝜑 → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))

Distinct variable groups:   𝑡,ℎ,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧   𝑤,𝐴,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑢, 𝑡, ℎ)   𝐴(𝑣, 𝑢, 𝑡, ℎ)

Proof of Theorem dfac5lem4

Dummy variables 𝑔 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3454	. . . . . 6 ⊢ 𝑧 ∈ V
2		neeq1 3017	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3		eqeq1 2764	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
4	3	rexbidv 3186	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
5	2, 4	anbi12d 644	. . . . . 6 ⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))))
6	1, 5	elab 3633	. . . . 5 ⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
7	6	simplbi 502	. . . 4 ⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8		dfac5lem.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
9	7, 8	eleq2s 2878	. . 3 ⊢ (𝑧 ∈ 𝐴 → 𝑧 ≠ ∅)
10	9	rgen 3078	. 2 ⊢ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅
11		df-an 402	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ↔ ¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))
12	1, 5, 8	elab2 3636	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
13	12	simprbi 503	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))
14		vex 3454	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
15		neeq1 3017	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16		eqeq1 2764	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
17	16	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))
18	15, 17	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))))
19	14, 18, 8	elab2 3636	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))
20	19	simprbi 503	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))
21		sneq 4594	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑔 → {𝑡} = {𝑔})
22	21	xpeq1d 5684	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23		xpeq2 5676	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
24	22, 23	eqtrd 2795	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
25	24	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
26	25	cbvrexvw 3241	. . . . . . . . 9 ⊢ (∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔))
27	20, 26	sylib 221	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 → ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔))
28		eleq2 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ({𝑡} × 𝑡)))
29		elxp 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
30		opeq1 4833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → ⟨𝑢, 𝑣⟩ = ⟨𝑠, 𝑣⟩)
31	30	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑠, 𝑣⟩))
32		eleq1w 2843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑡} ↔ 𝑠 ∈ {𝑡}))
33	32	anbi1d 643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡) ↔ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
34	31, 33	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑠 → ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ↔ (𝑥 = ⟨𝑠, 𝑣⟩ ∧ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))))
35	34	excomimw 2077	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
36	29, 35	sylbi 220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑡} × 𝑡) → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
37	28, 36	biimtrdi 256	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))))
38		eleq2 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ({𝑔} × 𝑔)))
39		elxp 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
40		opeq1 4833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → ⟨𝑢, 𝑦⟩ = ⟨𝑠, 𝑦⟩)
41	40	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑠, 𝑦⟩))
42		eleq1w 2843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑔} ↔ 𝑠 ∈ {𝑔}))
43	42	anbi1d 643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔) ↔ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
44	41, 43	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑠 → ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) ↔ (𝑥 = ⟨𝑠, 𝑦⟩ ∧ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
45	44	excomimw 2077	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
46	39, 45	sylbi 220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑔} × 𝑔) → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
47	38, 46	biimtrdi 256	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
48	37, 47	im2anan9 632	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))))
49		exdistrv 1988	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) ↔ (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
50	48, 49	imbitrrdi 255	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))))
51		velsn 4600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
52		opeq1 4833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
53	52	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
54	53	biimpac 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
55	51, 54	sylan2b 606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
56	55	adantrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
57	56	exlimiv 1963	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
58		velsn 4600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
59		opeq1 4833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
60	59	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
61	60	biimpac 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
62	58, 61	sylan2b 606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
63	62	adantrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
64	63	exlimiv 1963	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
65	57, 64	sylan9req 2816	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
66		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑡 ∈ V
67		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
68	66, 67	opth1 5451	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
69	65, 68	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔)
70	69	exlimivv 1965	. . . . . . . . . . . . . . 15 ⊢ (∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔)
71	50, 70	syl6 36	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑡 = 𝑔))
72	71, 24	syl6 36	. . . . . . . . . . . . 13 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
73		eqeq12 2777	. . . . . . . . . . . . 13 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
74	72, 73	sylibrd 262	. . . . . . . . . . . 12 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
75	74	ex 418	. . . . . . . . . . 11 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
76	75	rexlimivw 3159	. . . . . . . . . 10 ⊢ (∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
77	76	rexlimdvw 3168	. . . . . . . . 9 ⊢ (∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
78	77	imp 412	. . . . . . . 8 ⊢ ((∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
79	13, 27, 78	syl2an 608	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
80	11, 79	biimtrrid 246	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
81	80	necon1ad 2972	. . . . 5 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)))
82	81	alrimdv 1962	. . . 4 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)))
83		disj1 4405	. . . 4 ⊢ ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))
84	82, 83	imbitrrdi 255	. . 3 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
85	84	rgen2 3202	. 2 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)
86		dfac5lem.2	. . 3 ⊢ (𝜑 ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
87		vex 3454	. . . . . . . 8 ⊢ ℎ ∈ V
88		vuniex 7742	. . . . . . . 8 ⊢ ∪ ℎ ∈ V
89	87, 88	xpex 7753	. . . . . . 7 ⊢ (ℎ × ∪ ℎ) ∈ V
90	89	pwex 5345	. . . . . 6 ⊢ 𝒫 (ℎ × ∪ ℎ) ∈ V
91		snssi 4746	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℎ → {𝑡} ⊆ ℎ)
92		elssuni 4899	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℎ → 𝑡 ⊆ ∪ ℎ)
93		xpss12 5670	. . . . . . . . . . . 12 ⊢ (({𝑡} ⊆ ℎ ∧ 𝑡 ⊆ ∪ ℎ) → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
94	91, 92, 93	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
95		vsnex 5400	. . . . . . . . . . . . 13 ⊢ {𝑡} ∈ V
96	95, 66	xpex 7753	. . . . . . . . . . . 12 ⊢ ({𝑡} × 𝑡) ∈ V
97	96	elpw 4561	. . . . . . . . . . 11 ⊢ (({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
98	94, 97	sylibr 237	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ))
99		eleq1 2848	. . . . . . . . . 10 ⊢ (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ)))
100	98, 99	syl5ibrcom 250	. . . . . . . . 9 ⊢ (𝑡 ∈ ℎ → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ)))
101	100	rexlimiv 3156	. . . . . . . 8 ⊢ (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))
102	101	adantl 487	. . . . . . 7 ⊢ ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))
103	102	abssi 4016	. . . . . 6 ⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 (ℎ × ∪ ℎ)
104	90, 103	ssexi 5287	. . . . 5 ⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ∈ V
105	8, 104	eqeltri 2856	. . . 4 ⊢ 𝐴 ∈ V
106		raleq 3316	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅))
107		raleq 3316	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
108	107	raleqbi1dv 3329	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
109	106, 108	anbi12d 644	. . . . 5 ⊢ (𝑥 = 𝐴 → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
110		raleq 3316	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
111	110	exbidv 1954	. . . . 5 ⊢ (𝑥 = 𝐴 → (∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
112	109, 111	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐴 → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))))
113	105, 112	spcv 3559	. . 3 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
114	86, 113	sylbi 220	. 2 ⊢ (𝜑 → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
115	10, 85, 114	mp2ani 711	1 ⊢ (𝜑 → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃!weu 2593  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ⟨cop 4590  ∪ cuni 4867   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-opab 5168  df-xp 5661  df-rel 5662

This theorem is used by:  dfac5lem5  10131