Theorem dfac5lem4 10163

Description: Lemma for dfac5 10166. (Contributed by NM, 11-Apr-2004.) Avoid ax-11 2154. (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 3481	. . . . . 6 ⊢ 𝑧 ∈ V
2		neeq1 3000	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3		eqeq1 2738	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
4	3	rexbidv 3176	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
5	2, 4	anbi12d 632	. . . . . 6 ⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))))
6	1, 5	elab 3680	. . . . 5 ⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
7	6	simplbi 497	. . . 4 ⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8		dfac5lem.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
9	7, 8	eleq2s 2856	. . 3 ⊢ (𝑧 ∈ 𝐴 → 𝑧 ≠ ∅)
10	9	rgen 3060	. 2 ⊢ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅
11		df-an 396	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ↔ ¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))
12	1, 5, 8	elab2 3684	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))
13	12	simprbi 496	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))
14		vex 3481	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
15		neeq1 3000	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16		eqeq1 2738	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
17	16	rexbidv 3176	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))
18	15, 17	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))))
19	14, 18, 8	elab2 3684	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))
20	19	simprbi 496	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))
21		sneq 4640	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑔 → {𝑡} = {𝑔})
22	21	xpeq1d 5717	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23		xpeq2 5709	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
24	22, 23	eqtrd 2774	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
25	24	eqeq2d 2745	. . . . . . . . . 10 ⊢ (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
26	25	cbvrexvw 3235	. . . . . . . . 9 ⊢ (∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔))
27	20, 26	sylib 218	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 → ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔))
28		eleq2 2827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ({𝑡} × 𝑡)))
29		elxp 5711	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
30		opeq1 4877	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → ⟨𝑢, 𝑣⟩ = ⟨𝑠, 𝑣⟩)
31	30	eqeq2d 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑠, 𝑣⟩))
32		eleq1w 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑡} ↔ 𝑠 ∈ {𝑡}))
33	32	anbi1d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡) ↔ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
34	31, 33	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑠 → ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ↔ (𝑥 = ⟨𝑠, 𝑣⟩ ∧ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))))
35	34	excomimw 2040	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
36	29, 35	sylbi 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑡} × 𝑡) → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))
37	28, 36	biimtrdi 253	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 → ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))))
38		eleq2 2827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ({𝑔} × 𝑔)))
39		elxp 5711	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
40		opeq1 4877	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → ⟨𝑢, 𝑦⟩ = ⟨𝑠, 𝑦⟩)
41	40	eqeq2d 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑠, 𝑦⟩))
42		eleq1w 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑔} ↔ 𝑠 ∈ {𝑔}))
43	42	anbi1d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔) ↔ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
44	41, 43	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑠 → ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) ↔ (𝑥 = ⟨𝑠, 𝑦⟩ ∧ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
45	44	excomimw 2040	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
46	39, 45	sylbi 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑔} × 𝑔) → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))
47	38, 46	biimtrdi 253	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 → ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
48	37, 47	im2anan9 620	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))))
49		exdistrv 1952	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) ↔ (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))
50	48, 49	imbitrrdi 252	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))))
51		velsn 4646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
52		opeq1 4877	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
53	52	eqeq2d 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
54	53	biimpac 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
55	51, 54	sylan2b 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
56	55	adantrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
57	56	exlimiv 1927	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
58		velsn 4646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
59		opeq1 4877	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
60	59	eqeq2d 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
61	60	biimpac 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
62	58, 61	sylan2b 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
63	62	adantrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
64	63	exlimiv 1927	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
65	57, 64	sylan9req 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
66		vex 3481	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑡 ∈ V
67		vex 3481	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
68	66, 67	opth1 5485	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
69	65, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔)
70	69	exlimivv 1929	. . . . . . . . . . . . . . 15 ⊢ (∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔)
71	50, 70	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑡 = 𝑔))
72	71, 24	syl6 35	. . . . . . . . . . . . 13 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
73		eqeq12 2751	. . . . . . . . . . . . 13 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
74	72, 73	sylibrd 259	. . . . . . . . . . . 12 ⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
75	74	ex 412	. . . . . . . . . . 11 ⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
76	75	rexlimivw 3148	. . . . . . . . . 10 ⊢ (∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
77	76	rexlimdvw 3157	. . . . . . . . 9 ⊢ (∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)))
78	77	imp 406	. . . . . . . 8 ⊢ ((∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
79	13, 27, 78	syl2an 596	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
80	11, 79	biimtrrid 243	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))
81	80	necon1ad 2954	. . . . 5 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)))
82	81	alrimdv 1926	. . . 4 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)))
83		disj1 4457	. . . 4 ⊢ ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))
84	82, 83	imbitrrdi 252	. . 3 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
85	84	rgen2 3196	. 2 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)
86		dfac5lem.2	. . 3 ⊢ (𝜑 ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
87		vex 3481	. . . . . . . 8 ⊢ ℎ ∈ V
88		vuniex 7757	. . . . . . . 8 ⊢ ∪ ℎ ∈ V
89	87, 88	xpex 7771	. . . . . . 7 ⊢ (ℎ × ∪ ℎ) ∈ V
90	89	pwex 5385	. . . . . 6 ⊢ 𝒫 (ℎ × ∪ ℎ) ∈ V
91		snssi 4812	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℎ → {𝑡} ⊆ ℎ)
92		elssuni 4941	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℎ → 𝑡 ⊆ ∪ ℎ)
93		xpss12 5703	. . . . . . . . . . . 12 ⊢ (({𝑡} ⊆ ℎ ∧ 𝑡 ⊆ ∪ ℎ) → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
94	91, 92, 93	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
95		vsnex 5439	. . . . . . . . . . . . 13 ⊢ {𝑡} ∈ V
96	95, 66	xpex 7771	. . . . . . . . . . . 12 ⊢ ({𝑡} × 𝑡) ∈ V
97	96	elpw 4608	. . . . . . . . . . 11 ⊢ (({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ))
98	94, 97	sylibr 234	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ))
99		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ)))
100	98, 99	syl5ibrcom 247	. . . . . . . . 9 ⊢ (𝑡 ∈ ℎ → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ)))
101	100	rexlimiv 3145	. . . . . . . 8 ⊢ (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))
102	101	adantl 481	. . . . . . 7 ⊢ ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))
103	102	abssi 4079	. . . . . 6 ⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 (ℎ × ∪ ℎ)
104	90, 103	ssexi 5327	. . . . 5 ⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ∈ V
105	8, 104	eqeltri 2834	. . . 4 ⊢ 𝐴 ∈ V
106		raleq 3320	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅))
107		raleq 3320	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
108	107	raleqbi1dv 3335	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
109	106, 108	anbi12d 632	. . . . 5 ⊢ (𝑥 = 𝐴 → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))))
110		raleq 3320	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
111	110	exbidv 1918	. . . . 5 ⊢ (𝑥 = 𝐴 → (∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
112	109, 111	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))))
113	105, 112	spcv 3604	. . 3 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
114	86, 113	sylbi 217	. 2 ⊢ (𝜑 → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
115	10, 85, 114	mp2ani 698	1 ⊢ (𝜑 → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105  ∃!weu 2565  {cab 2711   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  Vcvv 3477   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338  𝒫 cpw 4604  {csn 4630  ⟨cop 4636  ∪ cuni 4911   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  dfac5lem5  10164