Theorem kmlem14 10166

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 3023	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 𝑤 ↔ 𝑦 ≠ 𝑤))
2		ineq1 4169	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∩ 𝑤) = (𝑦 ∩ 𝑤))
3	2	eleq2d 2852	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ 𝑣 ∈ (𝑦 ∩ 𝑤)))
4	1, 3	anbi12d 644	. . . . 5 ⊢ (𝑧 = 𝑦 → ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
5	4	rexbidv 3192	. . . 4 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
6	5	raleqbi1dv 3336	. . 3 ⊢ (𝑧 = 𝑦 → (∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
7	6	cbvrexvw 3247	. 2 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)))
8		df-rex 3093	. 2 ⊢ (∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
9		eleq1w 2849	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑤)))
10	9	anbi2d 642	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → ((𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
11	10	rexbidv 3192	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
12	11	cbvralvw 3246	. . . . . 6 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))
13		df-ral 3083	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
14	12, 13	bitri 278	. . . . 5 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
15	14	anbi2i 635	. . . 4 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
16		19.28v 2029	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
17		neeq2 3024	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑦 ≠ 𝑤 ↔ 𝑦 ≠ 𝑣))
18		ineq2 4170	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → (𝑦 ∩ 𝑤) = (𝑦 ∩ 𝑣))
19	18	eleq2d 2852	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑧 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
20	17, 19	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → ((𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
21	20	cbvrexvw 3247	. . . . . . . . . 10 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))
22		df-rex 3093	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
23	21, 22	bitri 278	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
24	23	imbi2i 339	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
25		19.37v 2030	. . . . . . . 8 ⊢ (∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
26	24, 25	bitr4i 281	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
27	26	anbi2i 635	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
28		19.42v 1986	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
29		19.3v 2015	. . . . . . . 8 ⊢ (∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ 𝜑))
30		kmlem14.1	. . . . . . . . . 10 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))
31		elin 3924	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑦 ∩ 𝑣) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝑣))
32	31	baibr 546	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
33	32	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
34		anass 474	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
35	33, 34	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
36	35	pm5.74i 274	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)) ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
37	30, 36	bitri 278	. . . . . . . . 9 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
38	37	anbi2i 635	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
39	29, 38	bitr2i 279	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
40	39	exbii 1881	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
41	27, 28, 40	3bitr2i 302	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
42	41	albii 1852	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
43	15, 16, 42	3bitr2i 302	. . 3 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
44	43	exbii 1881	. 2 ⊢ (∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
45	7, 8, 44	3bitri 300	1 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2146  ∃!weu 2599   ≠ wne 2961  ∀wral 3082  ∃wrex 3092   ∩ cin 3907

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-in 3915

This theorem is used by:  kmlem16  10168