Theorem dfac5lem4 10195

Description: Lemma for dfac5 10198. (Contributed by NM, 11-Apr-2004.) Avoid ax-11 2158. (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 3492	. . . . . 6 ⊢ 𝑧 ∈ V
2		neeq1 3009	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3		eqeq1 2744	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
4	3	rexbidv 3185	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
5	2, 4	anbi12d 631	. . . . . 6 ⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))))
6	1, 5	elab 3694	. . . . 5 ⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
7	6	simplbi 497	. . . 4 ⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8		dfac5lem.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
9	7, 8	eleq2s 2862	. . 3 ⊢ (𝑧 ∈ 𝐴 → 𝑧 ≠ ∅)
10	9	rgen 3069	. 2 ⊢ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅
11		df-an 396	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ↔ ¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))
12	1, 5, 8	elab2 3698	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
13	12	simprbi 496	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))
14		vex 3492	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
15		neeq1 3009	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16		eqeq1 2744	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
17	16	rexbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))
18	15, 17	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))))
19	14, 18, 8	elab2 3698	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))
20	19	simprbi 496	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))
21		sneq 4658	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑔 → {𝑡} = {𝑔})
22	21	xpeq1d 5729	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23		xpeq2 5721	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
24	22, 23	eqtrd 2780	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
25	24	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
26	25	cbvrexvw 3244	. . . . . . . . 9 ⊢ (∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔))
27	20, 26	sylib 218	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 → ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔))
28		eleq2 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ({𝑡} × 𝑡)))
29		elxp 5723	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
30		opeq1 4897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → ⟨𝑢, 𝑣⟩ = ⟨𝑠, 𝑣⟩)
31	30	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑠, 𝑣⟩))
32		eleq1w 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑡} ↔ 𝑠 ∈ {𝑡}))
33	32	anbi1d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡) ↔ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
34	31, 33	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑠 → ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ↔ (𝑥 = ⟨𝑠, 𝑣⟩ ∧ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))))
35	34	excomimw 2043	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
36	29, 35	sylbi 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑡} × 𝑡) → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
37	28, 36	biimtrdi 253	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))))
38		eleq2 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ({𝑔} × 𝑔)))
39		elxp 5723	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
40		opeq1 4897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → ⟨𝑢, 𝑦⟩ = ⟨𝑠, 𝑦⟩)
41	40	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑠, 𝑦⟩))
42		eleq1w 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑔} ↔ 𝑠 ∈ {𝑔}))
43	42	anbi1d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔) ↔ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
44	41, 43	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑠 → ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) ↔ (𝑥 = ⟨𝑠, 𝑦⟩ ∧ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
45	44	excomimw 2043	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
46	39, 45	sylbi 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑔} × 𝑔) → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
47	38, 46	biimtrdi 253	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
48	37, 47	im2anan9 619	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))))
49		exdistrv 1955	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) ↔ (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
50	48, 49	imbitrrdi 252	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))))
51		velsn 4664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
52		opeq1 4897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
53	52	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
54	53	biimpac 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
55	51, 54	sylan2b 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
56	55	adantrr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
57	56	exlimiv 1929	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
58		velsn 4664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
59		opeq1 4897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
60	59	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
61	60	biimpac 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
62	58, 61	sylan2b 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
63	62	adantrr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
64	63	exlimiv 1929	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
65	57, 64	sylan9req 2801	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
66		vex 3492	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑡 ∈ V
67		vex 3492	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
68	66, 67	opth1 5495	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
69	65, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔)
70	69	exlimivv 1931	. . . . . . . . . . . . . . 15 ⊢ (∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔)
71	50, 70	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑡 = 𝑔))
72	71, 24	syl6 35	. . . . . . . . . . . . 13 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
73		eqeq12 2757	. . . . . . . . . . . . 13 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
74	72, 73	sylibrd 259	. . . . . . . . . . . 12 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
75	74	ex 412	. . . . . . . . . . 11 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
76	75	rexlimivw 3157	. . . . . . . . . 10 ⊢ (∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
77	76	rexlimdvw 3166	. . . . . . . . 9 ⊢ (∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
78	77	imp 406	. . . . . . . 8 ⊢ ((∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
79	13, 27, 78	syl2an 595	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
80	11, 79	biimtrrid 243	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
81	80	necon1ad 2963	. . . . 5 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)))
82	81	alrimdv 1928	. . . 4 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)))
83		disj1 4475	. . . 4 ⊢ ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))
84	82, 83	imbitrrdi 252	. . 3 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
85	84	rgen2 3205	. 2 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)
86		dfac5lem.2	. . 3 ⊢ (𝜑 ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
87		vex 3492	. . . . . . . 8 ⊢ ℎ ∈ V
88		vuniex 7774	. . . . . . . 8 ⊢ ∪ ℎ ∈ V
89	87, 88	xpex 7788	. . . . . . 7 ⊢ (ℎ × ∪ ℎ) ∈ V
90	89	pwex 5398	. . . . . 6 ⊢ 𝒫 (ℎ × ∪ ℎ) ∈ V
91		snssi 4833	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℎ → {𝑡} ⊆ ℎ)
92		elssuni 4961	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℎ → 𝑡 ⊆ ∪ ℎ)
93		xpss12 5715	. . . . . . . . . . . 12 ⊢ (({𝑡} ⊆ ℎ ∧ 𝑡 ⊆ ∪ ℎ) → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
94	91, 92, 93	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
95		vsnex 5449	. . . . . . . . . . . . 13 ⊢ {𝑡} ∈ V
96	95, 66	xpex 7788	. . . . . . . . . . . 12 ⊢ ({𝑡} × 𝑡) ∈ V
97	96	elpw 4626	. . . . . . . . . . 11 ⊢ (({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
98	94, 97	sylibr 234	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ))
99		eleq1 2832	. . . . . . . . . 10 ⊢ (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ)))
100	98, 99	syl5ibrcom 247	. . . . . . . . 9 ⊢ (𝑡 ∈ ℎ → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ)))
101	100	rexlimiv 3154	. . . . . . . 8 ⊢ (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))
102	101	adantl 481	. . . . . . 7 ⊢ ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))
103	102	abssi 4093	. . . . . 6 ⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 (ℎ × ∪ ℎ)
104	90, 103	ssexi 5340	. . . . 5 ⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ∈ V
105	8, 104	eqeltri 2840	. . . 4 ⊢ 𝐴 ∈ V
106		raleq 3331	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅))
107		raleq 3331	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
108	107	raleqbi1dv 3346	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
109	106, 108	anbi12d 631	. . . . 5 ⊢ (𝑥 = 𝐴 → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
110		raleq 3331	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
111	110	exbidv 1920	. . . . 5 ⊢ (𝑥 = 𝐴 → (∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
112	109, 111	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))))
113	105, 112	spcv 3618	. . 3 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
114	86, 113	sylbi 217	. 2 ⊢ (𝜑 → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
115	10, 85, 114	mp2ani 697	1 ⊢ (𝜑 → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∃!weu 2571  {cab 2717   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  𝒫 cpw 4622  {csn 4648  ⟨cop 4654  ∪ cuni 4931   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  dfac5lem5  10196