cvmliftlem10 - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cvmliftlem10		Structured version Visualization version GIF version

Theorem cvmliftlem10 36226

Description: Lemma for cvmlift 36231. The function 𝐾 is going to be our complete lifted path, formed by unioning together all the 𝑄 functions (each of which is defined on one segment [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] of the interval). Here we prove by induction that 𝐾 is a continuous function and a lift of 𝐺 by applying cvmliftlem6 36222, cvmliftlem7 36223 (to show it is a function and a lift), cvmliftlem8 36224 (to show it is continuous), and cvmliftlem9 36225 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23642 gives that 𝐾 is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)

**Hypotheses**
Ref	Expression
cvmliftlem.1	⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
cvmliftlem.b	⊢ 𝐵 = ∪ 𝐶
cvmliftlem.x	⊢ 𝑋 = ∪ 𝐽
cvmliftlem.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
cvmliftlem.g	⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
cvmliftlem.p	⊢ (𝜑 → 𝑃 ∈ 𝐵)
cvmliftlem.e	⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
cvmliftlem.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
cvmliftlem.t	⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
cvmliftlem.a	⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1^st ‘(𝑇‘𝑘)))
cvmliftlem.l	⊢ 𝐿 = (topGen‘ran (,))
cvmliftlem.q	⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
cvmliftlem.k	⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)
cvmliftlem10.1	⊢ (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))

**Assertion**
Ref	Expression
cvmliftlem10	⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))

Distinct variable groups: 𝑣,𝑏,𝑧,𝐵 𝑗,𝑏,𝑘,𝑚,𝑛,𝑠,𝑢,𝑥,𝐹,𝑣,𝑧 𝑛,𝐿,𝑧 𝑃,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧 𝐶,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑧 𝜑,𝑗,𝑛,𝑠,𝑥,𝑧 𝑁,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧 𝑆,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧 𝑗,𝑋 𝐺,𝑏,𝑗,𝑘,𝑚,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧 𝑇,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧 𝐽,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧 𝑄,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧 Allowed substitution hints: 𝜑(𝑣, 𝑢, 𝑘, 𝑚, 𝑏) 𝜒(𝑥, 𝑧, 𝑣, 𝑢, 𝑗, 𝑘, 𝑚, 𝑛, 𝑠, 𝑏) 𝐵(𝑥, 𝑢, 𝑗, 𝑘, 𝑚, 𝑛, 𝑠) 𝐶(𝑥, 𝑚) 𝑃(𝑗, 𝑠) 𝑄(𝑗, 𝑠) 𝑆(𝑚) 𝑇(𝑛) 𝐽(𝑚) 𝐾(𝑥, 𝑧, 𝑣, 𝑢, 𝑗, 𝑘, 𝑚, 𝑛, 𝑠, 𝑏) 𝐿(𝑥, 𝑣, 𝑢, 𝑗, 𝑘, 𝑚, 𝑠, 𝑏) 𝑁(𝑗, 𝑠) 𝑋(𝑥, 𝑧, 𝑣, 𝑢, 𝑘, 𝑚, 𝑛, 𝑠, 𝑏)

Proof of Theorem cvmliftlem10 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvmliftlem.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2		nnuz 13031	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
3	1, 2	eleqtrdi 2874	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
4		eluzfz2 13692	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
5	3, 4	syl 18	. 2 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
6		eleq1 2852	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7		oveq2 7451	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (1...𝑦) = (1...1))
8		1z 12753	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
9		fzsn 13727	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	8, 9	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
11	7, 10	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (1...𝑦) = {1})
12	11	iuneq1d 4982	. . . . . . . . 9 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ {1} (𝑄‘𝑘))
13		1ex 11330	. . . . . . . . . 10 ⊢ 1 ∈ V
14		fveq2 6908	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1))
15	13, 14	iunxsn 5054	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ {1} (𝑄‘𝑘) = (𝑄‘1)
16	12, 15	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = (𝑄‘1))
17		oveq1 7450	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
18	17	oveq2d 7459	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
19	18	oveq2d 7459	. . . . . . . . 9 ⊢ (𝑦 = 1 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
20	19	oveq1d 7458	. . . . . . . 8 ⊢ (𝑦 = 1 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
21	16, 20	eleq12d 2858	. . . . . . 7 ⊢ (𝑦 = 1 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶)))
22	16	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ (𝑄‘1)))
23	18	reseq2d 5981	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
24	22, 23	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = 1 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
25	21, 24	anbi12d 644	. . . . . 6 ⊢ (𝑦 = 1 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
26	6, 25	imbi12d 347	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))
27	26	imbi2d 343	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))))
28		eleq1 2852	. . . . . 6 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29		oveq2 7451	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
30	29	iuneq1d 4982	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
31		oveq1 7450	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	31	oveq2d 7459	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
33	32	oveq2d 7459	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
34	33	oveq1d 7458	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
35	30, 34	eleq12d 2858	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
36	30	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)))
37	32	reseq2d 5981	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
38	36, 37	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = 𝑛 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
39	35, 38	anbi12d 644	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
40	28, 39	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
41	40	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))))
42		eleq1 2852	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43		oveq2 7451	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
44	43	iuneq1d 4982	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
45		oveq1 7450	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
46	45	oveq2d 7459	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
47	46	oveq2d 7459	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
48	47	oveq1d 7458	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
49	44, 48	eleq12d 2858	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
50	44	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
51	46	reseq2d 5981	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
52	50, 51	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
53	49, 52	anbi12d 644	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
54	42, 53	imbi12d 347	. . . . 5 ⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
55	54	imbi2d 343	. . . 4 ⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
56		eleq1 2852	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57		oveq2 7451	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
58	57	iuneq1d 4982	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘))
59		cvmliftlem.k	. . . . . . . . 9 ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)
60	58, 59	eqtr4di 2816	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = 𝐾)
61		oveq1 7450	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
62	61	oveq2d 7459	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
63	62	oveq2d 7459	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑁 / 𝑁))))
64	63	oveq1d 7458	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶))
65	60, 64	eleq12d 2858	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
66	60	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ 𝐾))
67	62	reseq2d 5981	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
68	66, 67	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = 𝑁 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
69	65, 68	anbi12d 644	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
70	56, 69	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
71	70	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))))
72		eluzfz1 13691	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑁))
73	3, 72	syl 18	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (1...𝑁))
74		cvmliftlem.1	. . . . . . . . 9 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
75		cvmliftlem.b	. . . . . . . . 9 ⊢ 𝐵 = ∪ 𝐶
76		cvmliftlem.x	. . . . . . . . 9 ⊢ 𝑋 = ∪ 𝐽
77		cvmliftlem.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
78		cvmliftlem.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
79		cvmliftlem.p	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
80		cvmliftlem.e	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
81		cvmliftlem.t	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
82		cvmliftlem.a	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1^st ‘(𝑇‘𝑘)))
83		cvmliftlem.l	. . . . . . . . 9 ⊢ 𝐿 = (topGen‘ran (,))
84		cvmliftlem.q	. . . . . . . . 9 ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
85		eqid 2763	. . . . . . . . 9 ⊢ (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
86	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem8 36224	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
87	73, 86	mpdan 700	. . . . . . 7 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88		1m1e0 12442	. . . . . . . . . . . 12 ⊢ (1 − 1) = 0
89	88	oveq1i 7453	. . . . . . . . . . 11 ⊢ ((1 − 1) / 𝑁) = (0 / 𝑁)
90	1	nncnd 12378	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
91	1	nnne0d 12415	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ≠ 0)
92	90, 91	div0d 12119	. . . . . . . . . . 11 ⊢ (𝜑 → (0 / 𝑁) = 0)
93	89, 92	eqtrid 2810	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 1) / 𝑁) = 0)
94	93	oveq1d 7458	. . . . . . . . 9 ⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
95	94	oveq2d 7459	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
96	95	oveq1d 7458	. . . . . . 7 ⊢ (𝜑 → ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
97	87, 96	eleqtrd 2866	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
98		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁))
99	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem7 36223	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((1 − 1) / 𝑁))}))
100	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99	cvmliftlem6 36222	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
101	73, 100	mpdan 700	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
102	101	simprd 501	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))
103	94	reseq2d 5981	. . . . . . 7 ⊢ (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104	102, 103	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))
105	97, 104	jca 521	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
106	105	a1d 26	. . . 4 ⊢ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
107		elnnuz 13032	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
108	107	biimpi 219	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
109	108	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
110		peano2fzr 13697	. . . . . . . 8 ⊢ ((𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
111	110	ex 418	. . . . . . 7 ⊢ (𝑛 ∈ (ℤ_≥‘1) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
112	109, 111	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
113	112	imim1d 83	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
114		cvmliftlem10.1	. . . . . . 7 ⊢ (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
115		eqid 2763	. . . . . . . . 9 ⊢ ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))
116		0re 11337	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
117	114	simplbi 502	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
118	117	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
119	118	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ (1...𝑁))
120		elfznn 13714	. . . . . . . . . . . . . 14 ⊢ ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121	119, 120	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℕ)
122	121	nnred 12377	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℝ)
123	1	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℕ)
124	122, 123	nndivred 12419	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125		iccssre 13587	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
126	116, 124, 125	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
127	117	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑛 ∈ ℕ)
128	127	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ)
129	128	nnred 12377	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℝ)
130	129, 123	nndivred 12419	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131		icccld 25115	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132	116, 130, 131	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
133	83	fveq2i 6911	. . . . . . . . . . 11 ⊢ (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134	132, 133	eleqtrrdi 2875	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135		ssun1 4179	. . . . . . . . . . 11 ⊢ (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136	116	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ)
137	128	nnnn0d 12694	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ₀)
138	137	nn0ge0d 12697	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ 𝑛)
139	123	nnred 12377	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℝ)
140	123	nngt0d 12414	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 < 𝑁)
141		divge0 12213	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142	129, 138, 139, 140, 141	syl22anc 852	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ (𝑛 / 𝑁))
143	129	ltp1d 12274	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 < (𝑛 + 1))
144		ltdiv1 12208	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145	129, 122, 139, 140, 144	syl112anc 1402	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146	143, 145	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147	130, 124, 146	ltled 11485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148		elicc2 13569	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
149	116, 124, 148	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
150	130, 142, 147, 149	mpbir3and 1361	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151		iccsplit 13643	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152	136, 124, 150, 151	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153	135, 152	sseqtrrid 3956	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154		uniretop 25111	. . . . . . . . . . . 12 ⊢ ℝ = ∪ (topGen‘ran (,))
155	83	unieqi 4882	. . . . . . . . . . . 12 ⊢ ∪ 𝐿 = ∪ (topGen‘ran (,))
156	154, 155	eqtr4i 2789	. . . . . . . . . . 11 ⊢ ℝ = ∪ 𝐿
157	156	restcldi 23521	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
158	126, 134, 153, 157	syl3anc 1399	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
159		icccld 25115	. . . . . . . . . . . 12 ⊢ (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160	130, 124, 159	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161	160, 133	eleqtrrdi 2875	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162		ssun2 4180	. . . . . . . . . . 11 ⊢ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163	162, 152	sseqtrrid 3956	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164	156	restcldi 23521	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
165	126, 161, 163, 164	syl3anc 1399	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
166		retop 25110	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) ∈ Top
167	83, 166	eqeltri 2860	. . . . . . . . . . 11 ⊢ 𝐿 ∈ Top
168	156	restuni 23510	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
169	167, 126, 168	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
170	152, 169	eqtr3d 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
171	114	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
172	171	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
173	172	simpld 500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
174		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))
175	174, 75	cnf 23594	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
176	173, 175	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
177		iccssre 13587	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178	116, 130, 177	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179	156	restuni 23510	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
180	167, 178, 179	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
181	180	feq2d 6715	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵))
182	176, 181	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁))
185	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem7 36223	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}))
186	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185	cvmliftlem6 36222	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187	119, 186	syldan 603	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188	187	simpld 500	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
189	128	nncnd 12378	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℂ)
190		ax-1cn 11285	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
191		pncan 11590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192	189, 190, 191	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193	192	oveq1d 7458	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194	193	oveq1d 7458	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195	194	feq2d 6715	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196	188, 195	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197	176	ffund 6736	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
198	128, 108	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (ℤ_≥‘1))
199		eluzfz2 13692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ (1...𝑛))
200	198, 199	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑛))
201		fveq2 6908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝑄‘𝑘) = (𝑄‘𝑛))
202	201	ssiun2s 5010	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑛) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
203	200, 202	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
204		peano2rem 11652	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
205	129, 204	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) ∈ ℝ)
206	205, 123	nndivred 12419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
207	206	rexrd 11386	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ^*)
208	130	rexrd 11386	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ^*)
209	129	ltm1d 12276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) < 𝑛)
210		ltdiv1 12208	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
211	205, 129, 139, 140, 210	syl112anc 1402	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
212	209, 211	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))
213	206, 130, 212	ltled 11485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
214		ubicc2 13623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 − 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
215	207, 208, 213, 214	syl3anc 1399	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216	198, 119, 110	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑁))
217		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
218		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
219	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217	cvmliftlem7 36223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
220	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219	cvmliftlem6 36222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
221	216, 220	syldan 603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222	221	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
223	222	fdmd 6742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → dom (𝑄‘𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
224	215, 223	eleqtrrd 2867	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛))
225		funssfv 6929	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
226	197, 203, 224, 225	syl3anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
227	192	fveq2d 6912	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
228	227, 193	fveq12d 6915	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
229	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84	cvmliftlem9 36225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
230	119, 229	syldan 603	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
231	193	fveq2d 6912	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
232	230, 231	eqtr3d 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
233	226, 228, 232	3eqtr2d 2804	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234	233	opeq2d 4850	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
235	234	sneqd 4596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
236	182	ffnd 6732	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)))
237		0xr 11383	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ^*
238	237	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ^*)
239		ubicc2 13623	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240	238, 208, 142, 239	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241		fnressn 7186	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
242	236, 240, 241	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
243	196	ffnd 6732	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244	124	rexrd 11386	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
245		lbicc2 13622	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246	208, 244, 147, 245	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247		fnressn 7186	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
248	243, 246, 247	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
249	235, 242, 248	3eqtr4d 2808	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
250		df-icc 13510	. . . . . . . . . . . . . . . . 17 ⊢ [,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
251		xrmaxle 13340	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
252		xrlemin 13341	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
253	250, 251, 252	ixxin 13520	. . . . . . . . . . . . . . . 16 ⊢ (((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^) ∧ ((𝑛 / 𝑁) ∈ ℝ^ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*)) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
254	238, 208, 208, 244, 253	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
255	142	iftrued 4493	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256	147	iftrued 4493	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257	255, 256	oveq12d 7461	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258		iccid 13548	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 / 𝑁) ∈ ℝ^* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259	208, 258	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260	254, 257, 259	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261	260	reseq2d 5981	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}))
262	260	reseq2d 5981	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
263	249, 261, 262	3eqtr4d 2808	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264		fresaun 6775	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
265	182, 196, 263, 264	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
266		fzsuc 13732	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
267	198, 266	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
268	267	iuneq1d 4982	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) = ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘))
269		iunxun 5057	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘))
270		ovex 7476	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 + 1) ∈ V
271		fveq2 6908	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑛 + 1)))
272	270, 271	iunxsn 5054	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘) = (𝑄‘(𝑛 + 1))
273	272	uneq2i 4167	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
274	269, 273	eqtri 2786	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
275	268, 274	eqtr2di 2815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
276	275	feq1d 6713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
277	265, 276	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
278	170	feq2d 6715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
279	277, 278	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
280	275	reseq1d 5980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))))
281		fresaunres1 6777	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
282	182, 196, 263, 281	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
283	280, 282	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
284	167	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝐿 ∈ Top)
285		ovex 7476	. . . . . . . . . . . . 13 ⊢ (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286	285	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287		restabs 23513	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
288	284, 153, 286, 287	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
289	288	oveq1d 7458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
290	173, 283, 289	3eltr4d 2879	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) ∈ (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
291	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem8 36224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
292	119, 291	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
293	194	oveq2d 7459	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294	293	oveq1d 7458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
295	292, 294	eleqtrd 2866	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296	275	reseq1d 5980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297		fresaunres2 6776	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
298	182, 196, 263, 297	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
299	296, 298	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
300		restabs 23513	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301	284, 163, 286, 300	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
302	301	oveq1d 7458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
303	295, 299, 302	3eltr4d 2879	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
304	115, 75, 158, 165, 170, 279, 290, 303	paste 23642	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
305	152	reseq2d 5981	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306	172	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
307	187	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308	194	reseq2d 5981	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309	307, 308	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310	306, 309	uneq12d 4171	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311		coundi 6261	. . . . . . . . . 10 ⊢ (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
312		resundi 5995	. . . . . . . . . 10 ⊢ (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313	310, 311, 312	3eqtr4g 2823	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314	275	coeq2d 5846	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
315	305, 313, 314	3eqtr2rd 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
316	304, 315	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
317	114, 316	sylan2br 607	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
318	317	expr 462	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
319	113, 318	animpimp2impd 860	. . . 4 ⊢ (𝑛 ∈ ℕ → ((𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
320	27, 41, 55, 71, 106, 319	nnind 12380	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
321	1, 320	mpcom 39	. 2 ⊢ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
322	5, 321	mpd 16	1 ⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ∀wral 3080 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∪ cun 4152 ∅c0 4281 ifcif 4485 𝒫 cpw 4560 {csn 4588 ⟨cop 4838 ∪ cuni 4870 ∪ ciun 4954 class class class wbr 5106 ↦ cmpt 5189 I cid 5549 × cxp 5653 ^◡ccnv 5654 dom cdm 5655 ran crn 5656 ↾ cres 5657 “ cima 5658 ∘ ccom 5659 Fun wfun 6552 Fn wfn 6553 ⟶wf 6554 ‘cfv 6558 ℩crio 7399 (class class class)co 7443 ∈ cmpo 7445 1^st c1st 8023 2^nd c2nd 8024 ℂcc 11225 ℝcr 11226 0cc0 11227 1c1 11228 + caddc 11230 ℝ^*cxr 11369 < clt 11370 ≤ cle 11371 − cmin 11568 / cdiv 12000 ℕcn 12362 ℤcz 12720 ℤ_≥cuz 12992 (,)cioo 13503 [,]cicc 13506 ...cfz 13666 seqcseq 14171 ↾_t crest 17620 topGenctg 17637 Topctop 23241 Clsdccld 23364 Cn ccn 23572 Homeochmeo 24102 IIcii 25226 CovMap ccvm 36187

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-er 8745 df-map 8877 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fi 9430 df-sup 9461 df-inf 9462 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-n0 12634 df-z 12721 df-uz 12993 df-q 13103 df-rp 13148 df-xneg 13268 df-xadd 13269 df-xmul 13270 df-ioo 13507 df-icc 13510 df-fz 13667 df-seq 14172 df-exp 14232 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-rest 17622 df-topgen 17643 df-psmet 21700 df-xmet 21701 df-met 21702 df-bl 21703 df-mopn 21704 df-top 23242 df-topon 23259 df-bases 23294 df-cld 23367 df-cn 23575 df-hmeo 24104 df-ii 25228 df-cvm 36188

This theorem is used by: cvmliftlem11 36227

W3C validator