cvmliftlem15 - Mathbox for Mario Carneiro

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

Theorem cvmliftlem15 35270

Description: Lemma for cvmlift 35271. Discharge the assumptions of cvmliftlem14 35269. The set of all open subsets 𝑢 of the unit interval such that 𝐺 “ 𝑢 is contained in an even covering of some open set in 𝐽 is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii 24881, there is a subdivision of the closed unit interval into 𝑁 equal parts such that each part is entirely contained within one such open set of 𝐽. Then using finite choice ac6sfi 9189 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 35269. (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))

**Assertion**
Ref	Expression
cvmliftlem15	⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))

Distinct variable groups: 𝑣,𝐵 𝑓,𝑘,𝑠,𝑢,𝑣,𝐹 𝑃,𝑓,𝑘,𝑢,𝑣 𝐶,𝑓,𝑘,𝑠,𝑢,𝑣 𝜑,𝑓,𝑠 𝑆,𝑓,𝑘,𝑠,𝑢,𝑣 𝑓,𝐺,𝑘,𝑠,𝑢,𝑣 𝑓,𝐽,𝑘,𝑠,𝑢,𝑣 Allowed substitution hints: 𝜑(𝑣,𝑢,𝑘) 𝐵(𝑢,𝑓,𝑘,𝑠) 𝑃(𝑠) 𝑋(𝑣,𝑢,𝑓,𝑘,𝑠)

Proof of Theorem cvmliftlem15 Dummy variables 𝑏 𝑦 𝑧 𝑎 𝑐 𝑔 𝑗 𝑚 𝑛 𝑡 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrab2 4033	. . 3 ⊢ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II
2		cvmliftlem.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
3	2	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝐺 ∈ (II Cn 𝐽))
4		simprl 770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑗 ∈ 𝐽)
5		cnima 23168	. . . . . . . . . 10 ⊢ ((𝐺 ∈ (II Cn 𝐽) ∧ 𝑗 ∈ 𝐽) → (^◡𝐺 “ 𝑗) ∈ II)
6	3, 4, 5	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (^◡𝐺 “ 𝑗) ∈ II)
7		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑥 ∈ (0[,]1))
8		simprrl 780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺‘𝑥) ∈ 𝑗)
9		iiuni 24790	. . . . . . . . . . . . . 14 ⊢ (0[,]1) = ∪ II
10		cvmliftlem.x	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
11	9, 10	cnf 23149	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋)
12	2, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(0[,]1)⟶𝑋)
13	12	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝐺:(0[,]1)⟶𝑋)
14		ffn 6656	. . . . . . . . . . 11 ⊢ (𝐺:(0[,]1)⟶𝑋 → 𝐺 Fn (0[,]1))
15		elpreima 6996	. . . . . . . . . . 11 ⊢ (𝐺 Fn (0[,]1) → (𝑥 ∈ (^◡𝐺 “ 𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺‘𝑥) ∈ 𝑗)))
16	13, 14, 15	3syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝑥 ∈ (^◡𝐺 “ 𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺‘𝑥) ∈ 𝑗)))
17	7, 8, 16	mpbir2and 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑥 ∈ (^◡𝐺 “ 𝑗))
18		simprrr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝑆‘𝑗) ≠ ∅)
19		ffun 6659	. . . . . . . . . . . . 13 ⊢ (𝐺:(0[,]1)⟶𝑋 → Fun 𝐺)
20		funimacnv 6567	. . . . . . . . . . . . 13 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ 𝑗)) = (𝑗 ∩ ran 𝐺))
21	13, 19, 20	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺 “ (^◡𝐺 “ 𝑗)) = (𝑗 ∩ ran 𝐺))
22		inss1 4190	. . . . . . . . . . . 12 ⊢ (𝑗 ∩ ran 𝐺) ⊆ 𝑗
23	21, 22	eqsstrdi 3982	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
24	23	ralrimivw 3125	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∀𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
25		r19.2z 4448	. . . . . . . . . 10 ⊢ (((𝑆‘𝑗) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗) → ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
26	18, 24, 25	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
27		eleq2 2817	. . . . . . . . . . 11 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ (^◡𝐺 “ 𝑗)))
28		imaeq2 6011	. . . . . . . . . . . . 13 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (𝐺 “ 𝑢) = (𝐺 “ (^◡𝐺 “ 𝑗)))
29	28	sseq1d 3969	. . . . . . . . . . . 12 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → ((𝐺 “ 𝑢) ⊆ 𝑗 ↔ (𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗))
30	29	rexbidv 3153	. . . . . . . . . . 11 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗 ↔ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗))
31	27, 30	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → ((𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ (𝑥 ∈ (^◡𝐺 “ 𝑗) ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)))
32	31	rspcev 3579	. . . . . . . . 9 ⊢ (((^◡𝐺 “ 𝑗) ∈ II ∧ (𝑥 ∈ (^◡𝐺 “ 𝑗) ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)) → ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
33	6, 17, 26, 32	syl12anc 836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
34		cvmliftlem.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
35	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
36	12	ffvelcdmda 7022	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝐺‘𝑥) ∈ 𝑋)
37		cvmliftlem.1	. . . . . . . . . 10 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
38	37, 10	cvmcov 35235	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺‘𝑥) ∈ 𝑋) → ∃𝑗 ∈ 𝐽 ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))
39	35, 36, 38	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ∃𝑗 ∈ 𝐽 ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))
40	33, 39	reximddv 3145	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
41		r19.42v 3161	. . . . . . . . 9 ⊢ (∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
42	41	rexbii 3076	. . . . . . . 8 ⊢ (∃𝑢 ∈ II ∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
43		rexcom 3258	. . . . . . . 8 ⊢ (∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II ∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
44		elunirab 4876	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ↔ ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
45	42, 43, 44	3bitr4i 303	. . . . . . 7 ⊢ (∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ 𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
46	40, 45	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → 𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
47	46	ex 412	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) → 𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗}))
48	47	ssrdv 3943	. . . 4 ⊢ (𝜑 → (0[,]1) ⊆ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
49		uniss 4869	. . . . . 6 ⊢ ({𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ ∪ II)
50	1, 49	mp1i 13	. . . . 5 ⊢ (𝜑 → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ ∪ II)
51	50, 9	sseqtrrdi 3979	. . . 4 ⊢ (𝜑 → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ (0[,]1))
52	48, 51	eqssd 3955	. . 3 ⊢ (𝜑 → (0[,]1) = ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
53		lebnumii 24881	. . 3 ⊢ (({𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II ∧ (0[,]1) = ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗}) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
54	1, 52, 53	sylancr 587	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
55		fzfi 13897	. . . . 5 ⊢ (1...𝑛) ∈ Fin
56		imaeq2 6011	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (𝐺 “ 𝑢) = (𝐺 “ 𝑣))
57	56	sseq1d 3969	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → ((𝐺 “ 𝑢) ⊆ 𝑗 ↔ (𝐺 “ 𝑣) ⊆ 𝑗))
58	57	2rexbidv 3194	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗 ↔ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗))
59	58	rexrab 3658	. . . . . . 7 ⊢ (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 ↔ ∃𝑣 ∈ II (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣))
60		vex 3442	. . . . . . . . . . . . 13 ⊢ 𝑗 ∈ V
61		vex 3442	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
62	60, 61	op1std 7941	. . . . . . . . . . . 12 ⊢ (𝑢 = ⟨𝑗, 𝑠⟩ → (1^st ‘𝑢) = 𝑗)
63	62	sseq2d 3970	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑗, 𝑠⟩ → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) ↔ (𝐺 “ 𝑣) ⊆ 𝑗))
64	63	rexiunxp 5787	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) ↔ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗)
65		imass2 6057	. . . . . . . . . . . 12 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺 “ 𝑣))
66		sstr2 3944	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺 “ 𝑣) → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
68	67	reximdv 3144	. . . . . . . . . 10 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
69	64, 68	biimtrrid 243	. . . . . . . . 9 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
70	69	impcom 407	. . . . . . . 8 ⊢ ((∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣) → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
71	70	rexlimivw 3126	. . . . . . 7 ⊢ (∃𝑣 ∈ II (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣) → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
72	59, 71	sylbi 217	. . . . . 6 ⊢ (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
73	72	ralimi 3066	. . . . 5 ⊢ (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
74		fveq2 6826	. . . . . . 7 ⊢ (𝑢 = (𝑔‘𝑘) → (1^st ‘𝑢) = (1^st ‘(𝑔‘𝑘)))
75	74	sseq2d 3970	. . . . . 6 ⊢ (𝑢 = (𝑔‘𝑘) → ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢) ↔ (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
76	75	ac6sfi 9189	. . . . 5 ⊢ (((1...𝑛) ∈ Fin ∧ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)) → ∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
77	55, 73, 76	sylancr 587	. . . 4 ⊢ (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
78		cvmliftlem.b	. . . . . . 7 ⊢ 𝐵 = ∪ 𝐶
79	34	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
80	2	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝐺 ∈ (II Cn 𝐽))
81		cvmliftlem.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
82	81	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑃 ∈ 𝐵)
83		cvmliftlem.e	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
84	83	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → (𝐹‘𝑃) = (𝐺‘0))
85		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑛 ∈ ℕ)
86		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
87		sneq 4589	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑎 → {𝑗} = {𝑎})
88		fveq2 6826	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑎 → (𝑆‘𝑗) = (𝑆‘𝑎))
89	87, 88	xpeq12d 5654	. . . . . . . . . 10 ⊢ (𝑗 = 𝑎 → ({𝑗} × (𝑆‘𝑗)) = ({𝑎} × (𝑆‘𝑎)))
90	89	cbviunv 4992	. . . . . . . . 9 ⊢ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) = ∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎))
91		feq3 6636	. . . . . . . . 9 ⊢ (∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) = ∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎)) → (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ↔ 𝑔:(1...𝑛)⟶∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎))))
92	90, 91	ax-mp 5	. . . . . . . 8 ⊢ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ↔ 𝑔:(1...𝑛)⟶∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎)))
93	86, 92	sylib 218	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑔:(1...𝑛)⟶∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎)))
94		simprr 772	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))
95		eqid 2729	. . . . . . 7 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
96		2fveq3 6831	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)) = (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)))
97	96	cbvmptv 5199	. . . . . . . . . 10 ⊢ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)))
98		eleq2 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑏 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐 ↔ (𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
99	98	cbvriotavw 7320	. . . . . . . . . . . . . . 15 ⊢ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)
100		fveq1 6825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑦‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑤 − 1) / 𝑛)))
101	100	eleq1d 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
102	101	riotabidv 7312	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
103	99, 102	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
104	103	reseq2d 5934	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
105	104	cnveqd 5822	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
106	105	fveq1d 6828	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)) = (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))
107	106	mpteq2dv 5189	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
108	97, 107	eqtrid 2776	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
109		oveq1 7360	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑚 → (𝑤 − 1) = (𝑚 − 1))
110	109	oveq1d 7368	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → ((𝑤 − 1) / 𝑛) = ((𝑚 − 1) / 𝑛))
111		oveq1 7360	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → (𝑤 / 𝑛) = (𝑚 / 𝑛))
112	110, 111	oveq12d 7371	. . . . . . . . . 10 ⊢ (𝑤 = 𝑚 → (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) = (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)))
113		2fveq3 6831	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑚 → (2^nd ‘(𝑔‘𝑤)) = (2^nd ‘(𝑔‘𝑚)))
114	110	fveq2d 6830	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑚 → (𝑥‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑚 − 1) / 𝑛)))
115	114	eleq1d 2813	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑚 → ((𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
116	113, 115	riotaeqbidv 7313	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑚 → (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
117	116	reseq2d 5934	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑚 → (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
118	117	cnveqd 5822	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
119	118	fveq1d 6828	. . . . . . . . . 10 ⊢ (𝑤 = 𝑚 → (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)) = (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))
120	112, 119	mpteq12dv 5182	. . . . . . . . 9 ⊢ (𝑤 = 𝑚 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
121	108, 120	cbvmpov 7448	. . . . . . . 8 ⊢ (𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
122		seqeq2 13930	. . . . . . . 8 ⊢ ((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))) → seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})) = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})))
123	121, 122	ax-mp 5	. . . . . . 7 ⊢ seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})) = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
124		eqid 2729	. . . . . . 7 ⊢ ∪ 𝑘 ∈ (1...𝑛)(seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘𝑘)
125	37, 78, 10, 79, 80, 82, 84, 85, 93, 94, 95, 123, 124	cvmliftlem14 35269	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
126	125	ex 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
127	126	exlimdv 1933	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
128	77, 127	syl5 34	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
129	128	rexlimdva 3130	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
130	54, 129	mpd 15	1 ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 ∃!wreu 3343 {crab 3396 Vcvv 3438 ∖ cdif 3902 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4553 {csn 4579 ⟨cop 4585 ∪ cuni 4861 ∪ ciun 4944 ↦ cmpt 5176 I cid 5517 × cxp 5621 ^◡ccnv 5622 ran crn 5624 ↾ cres 5625 “ cima 5626 ∘ ccom 5627 Fun wfun 6480 Fn wfn 6481 ⟶wf 6482 ‘cfv 6486 ℩crio 7309 (class class class)co 7353 ∈ cmpo 7355 1^st c1st 7929 2^nd c2nd 7930 Fincfn 8879 0cc0 11028 1c1 11029 − cmin 11365 / cdiv 11795 ℕcn 12146 (,)cioo 13266 [,]cicc 13269 ...cfz 13428 seqcseq 13926 ↾_t crest 17342 topGenctg 17359 Cn ccn 23127 Homeochmeo 23656 IIcii 24784 CovMap ccvm 35227

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8632 df-ec 8634 df-map 8762 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12610 df-uz 12754 df-q 12868 df-rp 12912 df-xneg 13032 df-xadd 13033 df-xmul 13034 df-ioo 13270 df-ico 13272 df-icc 13273 df-fz 13429 df-fzo 13576 df-fl 13714 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-clim 15413 df-sum 15612 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17344 df-topn 17345 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-prds 17369 df-xrs 17424 df-qtop 17429 df-imas 17430 df-xps 17432 df-mre 17506 df-mrc 17507 df-acs 17509 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-submnd 18676 df-mulg 18965 df-cntz 19214 df-cmn 19679 df-psmet 21271 df-xmet 21272 df-met 21273 df-bl 21274 df-mopn 21275 df-cnfld 21280 df-top 22797 df-topon 22814 df-topsp 22836 df-bases 22849 df-cld 22922 df-ntr 22923 df-cls 22924 df-nei 23001 df-cn 23130 df-cnp 23131 df-cmp 23290 df-conn 23315 df-lly 23369 df-nlly 23370 df-tx 23465 df-hmeo 23658 df-xms 24224 df-ms 24225 df-tms 24226 df-ii 24786 df-cncf 24787 df-htpy 24885 df-phtpy 24886 df-phtpc 24907 df-pconn 35193 df-sconn 35194 df-cvm 35228

This theorem is referenced by: cvmlift 35271

W3C validator