Theorem kmlem14 10135

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)

Hypotheses

Ref	Expression
kmlem14.1	⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))
kmlem14.2	⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))
kmlem14.3	⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))

Assertion

Ref	Expression
kmlem14	⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢   𝜑,𝑢

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣)   𝜓(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝜒(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)

Proof of Theorem kmlem14

Step	Hyp	Ref	Expression
1		neeq1 3022	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 𝑤 ↔ 𝑦 ≠ 𝑤))
2		ineq1 4168	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∩ 𝑤) = (𝑦 ∩ 𝑤))
3	2	eleq2d 2851	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ 𝑣 ∈ (𝑦 ∩ 𝑤)))
4	1, 3	anbi12d 643	. . . . 5 ⊢ (𝑧 = 𝑦 → ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
5	4	rexbidv 3189	. . . 4 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
6	5	raleqbi1dv 3333	. . 3 ⊢ (𝑧 = 𝑦 → (∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
7	6	cbvrexvw 3244	. 2 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)))
8		df-rex 3090	. 2 ⊢ (∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
9		eleq1w 2848	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑤)))
10	9	anbi2d 641	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → ((𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
11	10	rexbidv 3189	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
12	11	cbvralvw 3243	. . . . . 6 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))
13		df-ral 3080	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
14	12, 13	bitri 278	. . . . 5 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
15	14	anbi2i 634	. . . 4 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
16		19.28v 2019	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
17		neeq2 3023	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑦 ≠ 𝑤 ↔ 𝑦 ≠ 𝑣))
18		ineq2 4169	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → (𝑦 ∩ 𝑤) = (𝑦 ∩ 𝑣))
19	18	eleq2d 2851	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑧 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
20	17, 19	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → ((𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
21	20	cbvrexvw 3244	. . . . . . . . . 10 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))
22		df-rex 3090	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
23	21, 22	bitri 278	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
24	23	imbi2i 339	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
25		19.37v 2020	. . . . . . . 8 ⊢ (∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
26	24, 25	bitr4i 281	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
27	26	anbi2i 634	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
28		19.42v 1976	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
29		19.3v 2005	. . . . . . . 8 ⊢ (∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ 𝜑))
30		kmlem14.1	. . . . . . . . . 10 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))
31		elin 3923	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑦 ∩ 𝑣) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝑣))
32	31	baibr 545	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
33	32	anbi2d 641	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
34		anass 473	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
35	33, 34	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
36	35	pm5.74i 274	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)) ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
37	30, 36	bitri 278	. . . . . . . . 9 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
38	37	anbi2i 634	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
39	29, 38	bitr2i 279	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
40	39	exbii 1871	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
41	27, 28, 40	3bitr2i 302	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
42	41	albii 1842	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
43	15, 16, 42	3bitr2i 302	. . 3 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
44	43	exbii 1871	. 2 ⊢ (∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
45	7, 8, 44	3bitri 300	1 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561  ∃wex 1802   ∈ wcel 2145  ∃!weu 2598   ≠ wne 2960  ∀wral 3079  ∃wrex 3089   ∩ cin 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-in 3914

This theorem is referenced by:  kmlem16  10137