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 35266

Description: Lemma for cvmlift 35267. Discharge the assumptions of cvmliftlem14 35265. 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 25017, 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 9348 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 35265. (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 4103	. . 3 ⊢ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II
2		cvmliftlem.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
3	2	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝐺 ∈ (II Cn 𝐽))
4		simprl 770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑗 ∈ 𝐽)
5		cnima 23294	. . . . . . . . . 10 ⊢ ((𝐺 ∈ (II Cn 𝐽) ∧ 𝑗 ∈ 𝐽) → (^◡𝐺 “ 𝑗) ∈ II)
6	3, 4, 5	syl2anc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (^◡𝐺 “ 𝑗) ∈ II)
7		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑥 ∈ (0[,]1))
8		simprrl 780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺‘𝑥) ∈ 𝑗)
9		iiuni 24926	. . . . . . . . . . . . . 14 ⊢ (0[,]1) = ∪ II
10		cvmliftlem.x	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
11	9, 10	cnf 23275	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋)
12	2, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(0[,]1)⟶𝑋)
13	12	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝐺:(0[,]1)⟶𝑋)
14		ffn 6747	. . . . . . . . . . 11 ⊢ (𝐺:(0[,]1)⟶𝑋 → 𝐺 Fn (0[,]1))
15		elpreima 7091	. . . . . . . . . . 11 ⊢ (𝐺 Fn (0[,]1) → (𝑥 ∈ (^◡𝐺 “ 𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺‘𝑥) ∈ 𝑗)))
16	13, 14, 15	3syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝑥 ∈ (^◡𝐺 “ 𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺‘𝑥) ∈ 𝑗)))
17	7, 8, 16	mpbir2and 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑥 ∈ (^◡𝐺 “ 𝑗))
18		simprrr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝑆‘𝑗) ≠ ∅)
19		ffun 6750	. . . . . . . . . . . . 13 ⊢ (𝐺:(0[,]1)⟶𝑋 → Fun 𝐺)
20		funimacnv 6659	. . . . . . . . . . . . 13 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ 𝑗)) = (𝑗 ∩ ran 𝐺))
21	13, 19, 20	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺 “ (^◡𝐺 “ 𝑗)) = (𝑗 ∩ ran 𝐺))
22		inss1 4258	. . . . . . . . . . . 12 ⊢ (𝑗 ∩ ran 𝐺) ⊆ 𝑗
23	21, 22	eqsstrdi 4063	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
24	23	ralrimivw 3156	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∀𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
25		r19.2z 4518	. . . . . . . . . 10 ⊢ (((𝑆‘𝑗) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗) → ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
26	18, 24, 25	syl2anc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
27		eleq2 2833	. . . . . . . . . . 11 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ (^◡𝐺 “ 𝑗)))
28		imaeq2 6085	. . . . . . . . . . . . 13 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (𝐺 “ 𝑢) = (𝐺 “ (^◡𝐺 “ 𝑗)))
29	28	sseq1d 4040	. . . . . . . . . . . 12 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → ((𝐺 “ 𝑢) ⊆ 𝑗 ↔ (𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗))
30	29	rexbidv 3185	. . . . . . . . . . 11 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗 ↔ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗))
31	27, 30	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → ((𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ (𝑥 ∈ (^◡𝐺 “ 𝑗) ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)))
32	31	rspcev 3635	. . . . . . . . 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 7118	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝐺‘𝑥) ∈ 𝑋)
37		cvmliftlem.1	. . . . . . . . . 10 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
38	37, 10	cvmcov 35231	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺‘𝑥) ∈ 𝑋) → ∃𝑗 ∈ 𝐽 ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))
39	35, 36, 38	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ∃𝑗 ∈ 𝐽 ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))
40	33, 39	reximddv 3177	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
41		r19.42v 3197	. . . . . . . . 9 ⊢ (∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
42	41	rexbii 3100	. . . . . . . 8 ⊢ (∃𝑢 ∈ II ∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
43		rexcom 3296	. . . . . . . 8 ⊢ (∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II ∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
44		elunirab 4946	. . . . . . . 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 4014	. . . 4 ⊢ (𝜑 → (0[,]1) ⊆ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
49		uniss 4939	. . . . . 6 ⊢ ({𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ ∪ II)
50	1, 49	mp1i 13	. . . . 5 ⊢ (𝜑 → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ ∪ II)
51	50, 9	sseqtrrdi 4060	. . . 4 ⊢ (𝜑 → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ (0[,]1))
52	48, 51	eqssd 4026	. . 3 ⊢ (𝜑 → (0[,]1) = ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
53		lebnumii 25017	. . 3 ⊢ (({𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II ∧ (0[,]1) = ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗}) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
54	1, 52, 53	sylancr 586	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
55		fzfi 14023	. . . . 5 ⊢ (1...𝑛) ∈ Fin
56		imaeq2 6085	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (𝐺 “ 𝑢) = (𝐺 “ 𝑣))
57	56	sseq1d 4040	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → ((𝐺 “ 𝑢) ⊆ 𝑗 ↔ (𝐺 “ 𝑣) ⊆ 𝑗))
58	57	2rexbidv 3228	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗 ↔ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗))
59	58	rexrab 3718	. . . . . . 7 ⊢ (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 ↔ ∃𝑣 ∈ II (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣))
60		vex 3492	. . . . . . . . . . . . 13 ⊢ 𝑗 ∈ V
61		vex 3492	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
62	60, 61	op1std 8040	. . . . . . . . . . . 12 ⊢ (𝑢 = ⟨𝑗, 𝑠⟩ → (1^st ‘𝑢) = 𝑗)
63	62	sseq2d 4041	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑗, 𝑠⟩ → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) ↔ (𝐺 “ 𝑣) ⊆ 𝑗))
64	63	rexiunxp 5865	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) ↔ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗)
65		imass2 6132	. . . . . . . . . . . 12 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺 “ 𝑣))
66		sstr2 4015	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺 “ 𝑣) → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
68	67	reximdv 3176	. . . . . . . . . 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 3157	. . . . . . 7 ⊢ (∃𝑣 ∈ II (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣) → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
72	59, 71	sylbi 217	. . . . . 6 ⊢ (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
73	72	ralimi 3089	. . . . 5 ⊢ (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
74		fveq2 6920	. . . . . . 7 ⊢ (𝑢 = (𝑔‘𝑘) → (1^st ‘𝑢) = (1^st ‘(𝑔‘𝑘)))
75	74	sseq2d 4041	. . . . . 6 ⊢ (𝑢 = (𝑔‘𝑘) → ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢) ↔ (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
76	75	ac6sfi 9348	. . . . 5 ⊢ (((1...𝑛) ∈ Fin ∧ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)) → ∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
77	55, 73, 76	sylancr 586	. . . 4 ⊢ (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
78		cvmliftlem.b	. . . . . . 7 ⊢ 𝐵 = ∪ 𝐶
79	34	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
80	2	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝐺 ∈ (II Cn 𝐽))
81		cvmliftlem.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
82	81	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑃 ∈ 𝐵)
83		cvmliftlem.e	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
84	83	ad2antrr 725	. . . . . . 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 4658	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑎 → {𝑗} = {𝑎})
88		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑎 → (𝑆‘𝑗) = (𝑆‘𝑎))
89	87, 88	xpeq12d 5731	. . . . . . . . . 10 ⊢ (𝑗 = 𝑎 → ({𝑗} × (𝑆‘𝑗)) = ({𝑎} × (𝑆‘𝑎)))
90	89	cbviunv 5063	. . . . . . . . 9 ⊢ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) = ∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎))
91		feq3 6730	. . . . . . . . 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 2740	. . . . . . 7 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
96		2fveq3 6925	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)) = (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)))
97	96	cbvmptv 5279	. . . . . . . . . 10 ⊢ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)))
98		eleq2 2833	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑏 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐 ↔ (𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
99	98	cbvriotavw 7414	. . . . . . . . . . . . . . 15 ⊢ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)
100		fveq1 6919	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑦‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑤 − 1) / 𝑛)))
101	100	eleq1d 2829	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
102	101	riotabidv 7406	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
103	99, 102	eqtrid 2792	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
104	103	reseq2d 6009	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
105	104	cnveqd 5900	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
106	105	fveq1d 6922	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)) = (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))
107	106	mpteq2dv 5268	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
108	97, 107	eqtrid 2792	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
109		oveq1 7455	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑚 → (𝑤 − 1) = (𝑚 − 1))
110	109	oveq1d 7463	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → ((𝑤 − 1) / 𝑛) = ((𝑚 − 1) / 𝑛))
111		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → (𝑤 / 𝑛) = (𝑚 / 𝑛))
112	110, 111	oveq12d 7466	. . . . . . . . . 10 ⊢ (𝑤 = 𝑚 → (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) = (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)))
113		2fveq3 6925	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑚 → (2^nd ‘(𝑔‘𝑤)) = (2^nd ‘(𝑔‘𝑚)))
114	110	fveq2d 6924	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑚 → (𝑥‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑚 − 1) / 𝑛)))
115	114	eleq1d 2829	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑚 → ((𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
116	113, 115	riotaeqbidv 7407	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑚 → (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
117	116	reseq2d 6009	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑚 → (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
118	117	cnveqd 5900	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
119	118	fveq1d 6922	. . . . . . . . . 10 ⊢ (𝑤 = 𝑚 → (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)) = (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))
120	112, 119	mpteq12dv 5257	. . . . . . . . 9 ⊢ (𝑤 = 𝑚 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
121	108, 120	cbvmpov 7545	. . . . . . . 8 ⊢ (𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
122		seqeq2 14056	. . . . . . . 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 2740	. . . . . . 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 35265	. . . . . 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 1932	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
128	77, 127	syl5 34	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
129	128	rexlimdva 3161	. 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 1537 ∃wex 1777 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 ∃!wreu 3386 {crab 3443 Vcvv 3488 ∖ cdif 3973 ∪ cun 3974 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 𝒫 cpw 4622 {csn 4648 ⟨cop 4654 ∪ cuni 4931 ∪ ciun 5015 ↦ cmpt 5249 I cid 5592 × cxp 5698 ^◡ccnv 5699 ran crn 5701 ↾ cres 5702 “ cima 5703 ∘ ccom 5704 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 ‘cfv 6573 ℩crio 7403 (class class class)co 7448 ∈ cmpo 7450 1^st c1st 8028 2^nd c2nd 8029 Fincfn 9003 0cc0 11184 1c1 11185 − cmin 11520 / cdiv 11947 ℕcn 12293 (,)cioo 13407 [,]cicc 13410 ...cfz 13567 seqcseq 14052 ↾_t crest 17480 topGenctg 17497 Cn ccn 23253 Homeochmeo 23782 IIcii 24920 CovMap ccvm 35223

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-addf 11263

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-ec 8765 df-map 8886 df-ixp 8956 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-fi 9480 df-sup 9511 df-inf 9512 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-z 12640 df-dec 12759 df-uz 12904 df-q 13014 df-rp 13058 df-xneg 13175 df-xadd 13176 df-xmul 13177 df-ioo 13411 df-ico 13413 df-icc 13414 df-fz 13568 df-fzo 13712 df-fl 13843 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-clim 15534 df-sum 15735 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-rest 17482 df-topn 17483 df-0g 17501 df-gsum 17502 df-topgen 17503 df-pt 17504 df-prds 17507 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-submnd 18819 df-mulg 19108 df-cntz 19357 df-cmn 19824 df-psmet 21379 df-xmet 21380 df-met 21381 df-bl 21382 df-mopn 21383 df-cnfld 21388 df-top 22921 df-topon 22938 df-topsp 22960 df-bases 22974 df-cld 23048 df-ntr 23049 df-cls 23050 df-nei 23127 df-cn 23256 df-cnp 23257 df-cmp 23416 df-conn 23441 df-lly 23495 df-nlly 23496 df-tx 23591 df-hmeo 23784 df-xms 24351 df-ms 24352 df-tms 24353 df-ii 24922 df-cncf 24923 df-htpy 25021 df-phtpy 25022 df-phtpc 25043 df-pconn 35189 df-sconn 35190 df-cvm 35224

This theorem is referenced by: cvmlift 35267

W3C validator