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 36028

Description: Lemma for cvmlift 36033. 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 36024, cvmliftlem7 36025 (to show it is a function and a lift), cvmliftlem8 36026 (to show it is continuous), and cvmliftlem9 36027 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23592 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 12985	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
3	1, 2	eleqtrdi 2871	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
4		eluzfz2 13645	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
5	3, 4	syl 18	. 2 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
6		eleq1 2849	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (1...𝑦) = (1...1))
8		1z 12707	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
9		fzsn 13680	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	8, 9	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
11	7, 10	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (1...𝑦) = {1})
12	11	iuneq1d 4979	. . . . . . . . 9 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ {1} (𝑄‘𝑘))
13		1ex 11284	. . . . . . . . . 10 ⊢ 1 ∈ V
14		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1))
15	13, 14	iunxsn 5051	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ {1} (𝑄‘𝑘) = (𝑄‘1)
16	12, 15	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = (𝑄‘1))
17		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
18	17	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
19	18	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = 1 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
20	19	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = 1 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
21	16, 20	eleq12d 2855	. . . . . . 7 ⊢ (𝑦 = 1 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶)))
22	16	coeq2d 5840	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ (𝑄‘1)))
23	18	reseq2d 5970	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
24	22, 23	eqeq12d 2777	. . . . . . 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 2849	. . . . . 6 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29		oveq2 7420	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
30	29	iuneq1d 4979	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
31		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	31	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
33	32	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
34	33	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
35	30, 34	eleq12d 2855	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
36	30	coeq2d 5840	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)))
37	32	reseq2d 5970	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
38	36, 37	eqeq12d 2777	. . . . . . 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 2849	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43		oveq2 7420	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
44	43	iuneq1d 4979	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
45		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
46	45	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
47	46	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
48	47	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
49	44, 48	eleq12d 2855	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
50	44	coeq2d 5840	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
51	46	reseq2d 5970	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
52	50, 51	eqeq12d 2777	. . . . . . 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 2849	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57		oveq2 7420	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
58	57	iuneq1d 4979	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘))
59		cvmliftlem.k	. . . . . . . . 9 ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)
60	58, 59	eqtr4di 2814	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = 𝐾)
61		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
62	61	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
63	62	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑁 / 𝑁))))
64	63	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶))
65	60, 64	eleq12d 2855	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
66	60	coeq2d 5840	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ 𝐾))
67	62	reseq2d 5970	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
68	66, 67	eqeq12d 2777	. . . . . . 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 13644	. . . . . . . . 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 2761	. . . . . . . . 9 ⊢ (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
86	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem8 36026	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
87	73, 86	mpdan 700	. . . . . . 7 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88		1m1e0 12396	. . . . . . . . . . . 12 ⊢ (1 − 1) = 0
89	88	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((1 − 1) / 𝑁) = (0 / 𝑁)
90	1	nncnd 12332	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
91	1	nnne0d 12369	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ≠ 0)
92	90, 91	div0d 12073	. . . . . . . . . . 11 ⊢ (𝜑 → (0 / 𝑁) = 0)
93	89, 92	eqtrid 2808	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 1) / 𝑁) = 0)
94	93	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
95	94	oveq2d 7428	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
96	95	oveq1d 7427	. . . . . . 7 ⊢ (𝜑 → ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
97	87, 96	eleqtrd 2863	. . . . . 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 36025	. . . . . . . . . 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 36024	. . . . . . . . 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 5970	. . . . . . 7 ⊢ (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104	102, 103	eqtrd 2796	. . . . . 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 12986	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
108	107	biimpi 219	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
109	108	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
110		peano2fzr 13650	. . . . . . . 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 2761	. . . . . . . . 9 ⊢ ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))
116		0re 11291	. . . . . . . . . . 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 13667	. . . . . . . . . . . . . 14 ⊢ ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121	119, 120	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℕ)
122	121	nnred 12331	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℝ)
123	1	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℕ)
124	122, 123	nndivred 12373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125		iccssre 13541	. . . . . . . . . . 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 12331	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℝ)
130	129, 123	nndivred 12373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131		icccld 25065	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132	116, 130, 131	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
133	83	fveq2i 6880	. . . . . . . . . . 11 ⊢ (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134	132, 133	eleqtrrdi 2872	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135		ssun1 4124	. . . . . . . . . . 11 ⊢ (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136	116	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ)
137	128	nnnn0d 12648	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ₀)
138	137	nn0ge0d 12651	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ 𝑛)
139	123	nnred 12331	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℝ)
140	123	nngt0d 12368	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 < 𝑁)
141		divge0 12167	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142	129, 138, 139, 140, 141	syl22anc 852	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ (𝑛 / 𝑁))
143	129	ltp1d 12228	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 < (𝑛 + 1))
144		ltdiv1 12162	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145	129, 122, 139, 140, 144	syl112anc 1401	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146	143, 145	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147	130, 124, 146	ltled 11439	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148		elicc2 13523	. . . . . . . . . . . . . 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 13597	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152	136, 124, 150, 151	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153	135, 152	sseqtrrid 3974	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154		uniretop 25061	. . . . . . . . . . . 12 ⊢ ℝ = ∪ (topGen‘ran (,))
155	83	unieqi 4879	. . . . . . . . . . . 12 ⊢ ∪ 𝐿 = ∪ (topGen‘ran (,))
156	154, 155	eqtr4i 2787	. . . . . . . . . . 11 ⊢ ℝ = ∪ 𝐿
157	156	restcldi 23471	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
158	126, 134, 153, 157	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
159		icccld 25065	. . . . . . . . . . . 12 ⊢ (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160	130, 124, 159	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161	160, 133	eleqtrrdi 2872	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162		ssun2 4125	. . . . . . . . . . 11 ⊢ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163	162, 152	sseqtrrid 3974	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164	156	restcldi 23471	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
165	126, 161, 163, 164	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
166		retop 25060	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) ∈ Top
167	83, 166	eqeltri 2857	. . . . . . . . . . 11 ⊢ 𝐿 ∈ Top
168	156	restuni 23460	. . . . . . . . . . 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 2798	. . . . . . . . 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 2761	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))
175	174, 75	cnf 23544	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
176	173, 175	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
177		iccssre 13541	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178	116, 130, 177	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179	156	restuni 23460	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
180	167, 178, 179	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
181	180	feq2d 6685	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵))
182	176, 181	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183		eqid 2761	. . . . . . . . . . . . . . . 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 36025	. . . . . . . . . . . . . . . 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 36024	. . . . . . . . . . . . . . 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 12332	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℂ)
190		ax-1cn 11239	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
191		pncan 11544	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192	189, 190, 191	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193	192	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194	193	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195	194	feq2d 6685	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196	188, 195	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197	176	ffund 6706	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
198	128, 108	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (ℤ_≥‘1))
199		eluzfz2 13645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ (1...𝑛))
200	198, 199	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑛))
201		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝑄‘𝑘) = (𝑄‘𝑛))
202	201	ssiun2s 5007	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑛) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
203	200, 202	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
204		peano2rem 11606	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
205	129, 204	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) ∈ ℝ)
206	205, 123	nndivred 12373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
207	206	rexrd 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ^*)
208	130	rexrd 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ^*)
209	129	ltm1d 12230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) < 𝑛)
210		ltdiv1 12162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
211	205, 129, 139, 140, 210	syl112anc 1401	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
212	209, 211	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))
213	206, 130, 212	ltled 11439	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
214		ubicc2 13577	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 − 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
215	207, 208, 213, 214	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216	198, 119, 110	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑁))
217		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
218		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
219	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217	cvmliftlem7 36025	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
220	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219	cvmliftlem6 36024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
221	216, 220	syldan 603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222	221	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
223	222	fdmd 6712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → dom (𝑄‘𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
224	215, 223	eleqtrrd 2864	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛))
225		funssfv 6898	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
226	197, 203, 224, 225	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
227	192	fveq2d 6881	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
228	227, 193	fveq12d 6884	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
229	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84	cvmliftlem9 36027	. . . . . . . . . . . . . . . . . . 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 6881	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
232	230, 231	eqtr3d 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
233	226, 228, 232	3eqtr2d 2802	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234	233	opeq2d 4840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
235	234	sneqd 4596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
236	182	ffnd 6702	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)))
237		0xr 11337	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ^*
238	237	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ^*)
239		ubicc2 13577	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240	238, 208, 142, 239	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241		fnressn 7154	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
242	236, 240, 241	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
243	196	ffnd 6702	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244	124	rexrd 11340	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
245		lbicc2 13576	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246	208, 244, 147, 245	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247		fnressn 7154	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
248	243, 246, 247	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
249	235, 242, 248	3eqtr4d 2806	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
250		df-icc 13464	. . . . . . . . . . . . . . . . 17 ⊢ [,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
251		xrmaxle 13294	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
252		xrlemin 13295	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
253	250, 251, 252	ixxin 13474	. . . . . . . . . . . . . . . 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 4490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256	147	iftrued 4490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257	255, 256	oveq12d 7430	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258		iccid 13502	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 / 𝑁) ∈ ℝ^* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259	208, 258	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260	254, 257, 259	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261	260	reseq2d 5970	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}))
262	260	reseq2d 5970	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
263	249, 261, 262	3eqtr4d 2806	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264		fresaun 6745	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
265	182, 196, 263, 264	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
266		fzsuc 13685	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
267	198, 266	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
268	267	iuneq1d 4979	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) = ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘))
269		iunxun 5054	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘))
270		ovex 7445	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 + 1) ∈ V
271		fveq2 6877	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑛 + 1)))
272	270, 271	iunxsn 5051	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘) = (𝑄‘(𝑛 + 1))
273	272	uneq2i 4112	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
274	269, 273	eqtri 2784	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
275	268, 274	eqtr2di 2813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
276	275	feq1d 6683	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
277	265, 276	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
278	170	feq2d 6685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
279	277, 278	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
280	275	reseq1d 5969	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))))
281		fresaunres1 6747	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
282	182, 196, 263, 281	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
283	280, 282	eqtr3d 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
284	167	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝐿 ∈ Top)
285		ovex 7445	. . . . . . . . . . . . 13 ⊢ (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286	285	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287		restabs 23463	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
288	284, 153, 286, 287	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
289	288	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
290	173, 283, 289	3eltr4d 2876	. . . . . . . . 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 36026	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
292	119, 291	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
293	194	oveq2d 7428	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294	293	oveq1d 7427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
295	292, 294	eleqtrd 2863	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296	275	reseq1d 5969	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297		fresaunres2 6746	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
298	182, 196, 263, 297	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
299	296, 298	eqtr3d 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
300		restabs 23463	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301	284, 163, 286, 300	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
302	301	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
303	295, 299, 302	3eltr4d 2876	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
304	115, 75, 158, 165, 170, 279, 290, 303	paste 23592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
305	152	reseq2d 5970	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306	172	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
307	187	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308	194	reseq2d 5970	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309	307, 308	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310	306, 309	uneq12d 4116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311		coundi 6241	. . . . . . . . . 10 ⊢ (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
312		resundi 5984	. . . . . . . . . 10 ⊢ (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313	310, 311, 312	3eqtr4g 2821	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314	275	coeq2d 5840	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
315	305, 313, 314	3eqtr2rd 2803	. . . . . . . 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 12334	. . 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 2145 ∀wral 3077 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 ifcif 4482 𝒫 cpw 4557 {csn 4584 ⟨cop 4590 ∪ cuni 4867 ∪ ciun 4951 class class class wbr 5103 ↦ cmpt 5186 I cid 5545 × cxp 5649 ^◡ccnv 5650 dom cdm 5651 ran crn 5652 ↾ cres 5653 “ cima 5654 ∘ ccom 5655 Fun wfun 6525 Fn wfn 6526 ⟶wf 6527 ‘cfv 6531 ℩crio 7368 (class class class)co 7412 ∈ cmpo 7414 1^st c1st 7988 2^nd c2nd 7989 ℂcc 11179 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11522 / cdiv 11954 ℕcn 12316 ℤcz 12674 ℤ_≥cuz 12946 (,)cioo 13457 [,]cicc 13460 ...cfz 13620 seqcseq 14124 ↾_t crest 17571 topGenctg 17588 Topctop 23191 Clsdccld 23314 Cn ccn 23522 Homeochmeo 24052 IIcii 25176 CovMap ccvm 35989

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

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 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8701 df-map 8833 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fi 9387 df-sup 9418 df-inf 9419 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-n0 12588 df-z 12675 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-icc 13464 df-fz 13621 df-seq 14125 df-exp 14185 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-rest 17573 df-topgen 17594 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-top 23192 df-topon 23209 df-bases 23244 df-cld 23317 df-cn 23525 df-hmeo 24054 df-ii 25178 df-cvm 35990

This theorem is used by: cvmliftlem11 36029

W3C validator