Theorem kmlem14

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

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

Proof

Step	Hyp	Ref	Expression
1		kmlem14.1	⊢ ( 𝜑 ↔ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) )
2		kmlem14.2	⊢ ( 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
3		kmlem14.3	⊢ ( 𝜒 ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
4		neeq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ≠ 𝑤 ↔ 𝑦 ≠ 𝑤 ) )
5		ineq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∩ 𝑤 ) = ( 𝑦 ∩ 𝑤 ) )
6	5	eleq2d	⊢ ( 𝑧 = 𝑦 → ( 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ↔ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) )
7	4 6	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
8	7	rexbidv	⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
9	8	raleqbi1dv	⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
10	9	cbvrexvw	⊢ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) )
11		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑥 ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
12		eleq1w	⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ↔ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) )
13	12	anbi2d	⊢ ( 𝑣 = 𝑧 → ( ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
14	13	rexbidv	⊢ ( 𝑣 = 𝑧 → ( ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
15	14	cbvralvw	⊢ ( ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) )
16		df-ral	⊢ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
17	15 16	bitri	⊢ ( ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) )
18	17	anbi2i	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ) )
19		19.28v	⊢ ( ∀ 𝑧 ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ) )
20		neeq2	⊢ ( 𝑤 = 𝑣 → ( 𝑦 ≠ 𝑤 ↔ 𝑦 ≠ 𝑣 ) )
21		ineq2	⊢ ( 𝑤 = 𝑣 → ( 𝑦 ∩ 𝑤 ) = ( 𝑦 ∩ 𝑣 ) )
22	21	eleq2d	⊢ ( 𝑤 = 𝑣 → ( 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ↔ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) )
23	20 22	anbi12d	⊢ ( 𝑤 = 𝑣 → ( ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) )
24	23	cbvrexvw	⊢ ( ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ∃ 𝑣 ∈ 𝑥 ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) )
25		df-rex	⊢ ( ∃ 𝑣 ∈ 𝑥 ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) )
26	24 25	bitri	⊢ ( ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) )
27	26	imbi2i	⊢ ( ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ↔ ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) )
28		19.37v	⊢ ( ∃ 𝑣 ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) ↔ ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) )
29	27 28	bitr4i	⊢ ( ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) )
30	29	anbi2i	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑣 ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) ) )
31		19.42v	⊢ ( ∃ 𝑣 ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑣 ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) ) )
32		19.3v	⊢ ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
33		elin	⊢ ( 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝑣 ) )
34	33	baibr	⊢ ( 𝑧 ∈ 𝑦 → ( 𝑧 ∈ 𝑣 ↔ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) )
35	34	anbi2d	⊢ ( 𝑧 ∈ 𝑦 → ( ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ↔ ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) )
36		anass	⊢ ( ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) )
37	35 36	bitrdi	⊢ ( 𝑧 ∈ 𝑦 → ( ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) )
38	37	pm5.74i	⊢ ( ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) )
39	1 38	bitri	⊢ ( 𝜑 ↔ ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) )
40	39	anbi2i	⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) ) )
41	32 40	bitr2i	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) ) ↔ ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
42	41	exbii	⊢ ( ∃ 𝑣 ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( 𝑣 ∈ 𝑥 ∧ ( 𝑦 ≠ 𝑣 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑣 ) ) ) ) ) ↔ ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
43	30 31 42	3bitr2i	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ) ↔ ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
44	43	albii	⊢ ( ∀ 𝑧 ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑧 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
45	18 19 44	3bitr2i	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
46	45	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑣 ∈ 𝑦 ∃ 𝑤 ∈ 𝑥 ( 𝑦 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑦 ∩ 𝑤 ) ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
47	10 11 46	3bitri	⊢ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )