Theorem kmlem14 9850

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 3005	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 𝑤 ↔ 𝑦 ≠ 𝑤))
2		ineq1 4136	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∩ 𝑤) = (𝑦 ∩ 𝑤))
3	2	eleq2d 2824	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ 𝑣 ∈ (𝑦 ∩ 𝑤)))
4	1, 3	anbi12d 630	. . . . 5 ⊢ (𝑧 = 𝑦 → ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
5	4	rexbidv 3225	. . . 4 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
6	5	raleqbi1dv 3331	. . 3 ⊢ (𝑧 = 𝑦 → (∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
7	6	cbvrexvw 3373	. 2 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)))
8		df-rex 3069	. 2 ⊢ (∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
9		eleq1w 2821	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑤)))
10	9	anbi2d 628	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → ((𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
11	10	rexbidv 3225	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
12	11	cbvralvw 3372	. . . . . 6 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))
13		df-ral 3068	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
14	12, 13	bitri 274	. . . . 5 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
15	14	anbi2i 622	. . . 4 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
16		19.28v 1995	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
17		neeq2 3006	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑦 ≠ 𝑤 ↔ 𝑦 ≠ 𝑣))
18		ineq2 4137	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → (𝑦 ∩ 𝑤) = (𝑦 ∩ 𝑣))
19	18	eleq2d 2824	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑧 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
20	17, 19	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → ((𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
21	20	cbvrexvw 3373	. . . . . . . . . 10 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))
22		df-rex 3069	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
23	21, 22	bitri 274	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
24	23	imbi2i 335	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
25		19.37v 1996	. . . . . . . 8 ⊢ (∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
26	24, 25	bitr4i 277	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
27	26	anbi2i 622	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
28		19.42v 1958	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
29		19.3v 1986	. . . . . . . 8 ⊢ (∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ 𝜑))
30		kmlem14.1	. . . . . . . . . 10 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))
31		elin 3899	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑦 ∩ 𝑣) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝑣))
32	31	baibr 536	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
33	32	anbi2d 628	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
34		anass 468	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
35	33, 34	bitrdi 286	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
36	35	pm5.74i 270	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)) ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
37	30, 36	bitri 274	. . . . . . . . 9 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
38	37	anbi2i 622	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
39	29, 38	bitr2i 275	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
40	39	exbii 1851	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
41	27, 28, 40	3bitr2i 298	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
42	41	albii 1823	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
43	15, 16, 42	3bitr2i 298	. . 3 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
44	43	exbii 1851	. 2 ⊢ (∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
45	7, 8, 44	3bitri 296	1 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537  ∃wex 1783   ∈ wcel 2108  ∃!weu 2568   ≠ wne 2942  ∀wral 3063  ∃wrex 3064   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-in 3890

This theorem is referenced by:  kmlem16  9852