cvmliftlem1 - Mathbox for Mario Carneiro

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

Theorem cvmliftlem1 35520

Description: Lemma for cvmlift 35534. In cvmliftlem15 35533, we picked an 𝑁 large enough so that the sections (𝐺 “ [(𝑘 − 1) / 𝑁, 𝑘 / 𝑁]) are all contained in an even covering, and the function 𝑇 enumerates these even coverings. So 1^st ‘(𝑇‘𝑀) is a neighborhood of (𝐺 “ [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁]), and 2^nd ‘(𝑇‘𝑀) is an even covering of 1^st ‘(𝑇‘𝑀), which is to say a disjoint union of open sets in 𝐶 whose image is 1^st ‘(𝑇‘𝑀). (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 (,))
cvmliftlem1.m	⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))

**Assertion**
Ref	Expression
cvmliftlem1	⊢ ((𝜑 ∧ 𝜓) → (2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀))))

Distinct variable groups: 𝑣,𝐵 𝑗,𝑘,𝑠,𝑢,𝑣,𝐹 𝑗,𝑀,𝑘,𝑠,𝑢,𝑣 𝑃,𝑘,𝑢,𝑣 𝐶,𝑗,𝑘,𝑠,𝑢,𝑣 𝜑,𝑗,𝑠 𝑘,𝑁,𝑢,𝑣 𝑆,𝑗,𝑘,𝑠,𝑢,𝑣 𝑗,𝑋 𝑗,𝐺,𝑘,𝑠,𝑢,𝑣 𝑇,𝑗,𝑘,𝑠,𝑢,𝑣 𝑗,𝐽,𝑘,𝑠,𝑢,𝑣 Allowed substitution hints: 𝜑(𝑣,𝑢,𝑘) 𝜓(𝑣,𝑢,𝑗,𝑘,𝑠) 𝐵(𝑢,𝑗,𝑘,𝑠) 𝑃(𝑗,𝑠) 𝐿(𝑣,𝑢,𝑗,𝑘,𝑠) 𝑁(𝑗,𝑠) 𝑋(𝑣,𝑢,𝑘,𝑠)

**Proof of Theorem cvmliftlem1**
Step	Hyp	Ref	Expression
1		relxp 5643	. . . . . 6 ⊢ Rel ({𝑗} × (𝑆‘𝑗))
2	1	rgenw 3058	. . . . 5 ⊢ ∀𝑗 ∈ 𝐽 Rel ({𝑗} × (𝑆‘𝑗))
3		reliun 5766	. . . . 5 ⊢ (Rel ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ↔ ∀𝑗 ∈ 𝐽 Rel ({𝑗} × (𝑆‘𝑗)))
4	2, 3	mpbir 232	. . . 4 ⊢ Rel ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))
5		cvmliftlem.t	. . . . . 6 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
6	5	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
7		cvmliftlem1.m	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))
8	6, 7	ffvelcdmd 7033	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑇‘𝑀) ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
9		1st2nd 7988	. . . 4 ⊢ ((Rel ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ (𝑇‘𝑀) ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) → (𝑇‘𝑀) = ⟨(1^st ‘(𝑇‘𝑀)), (2^nd ‘(𝑇‘𝑀))⟩)
10	4, 8, 9	sylancr 593	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑇‘𝑀) = ⟨(1^st ‘(𝑇‘𝑀)), (2^nd ‘(𝑇‘𝑀))⟩)
11	10, 8	eqeltrrd 2841	. 2 ⊢ ((𝜑 ∧ 𝜓) → ⟨(1^st ‘(𝑇‘𝑀)), (2^nd ‘(𝑇‘𝑀))⟩ ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
12		fveq2 6834	. . . 4 ⊢ (𝑗 = (1^st ‘(𝑇‘𝑀)) → (𝑆‘𝑗) = (𝑆‘(1^st ‘(𝑇‘𝑀))))
13	12	opeliunxp2 5787	. . 3 ⊢ (⟨(1^st ‘(𝑇‘𝑀)), (2^nd ‘(𝑇‘𝑀))⟩ ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ↔ ((1^st ‘(𝑇‘𝑀)) ∈ 𝐽 ∧ (2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀)))))
14	13	simprbi 498	. 2 ⊢ (⟨(1^st ‘(𝑇‘𝑀)), (2^nd ‘(𝑇‘𝑀))⟩ ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) → (2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀))))
15	11, 14	syl 17	1 ⊢ ((𝜑 ∧ 𝜓) → (2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ∀wral 3054 {crab 3392 ∖ cdif 3887 ∩ cin 3889 ⊆ wss 3890 ∅c0 4268 𝒫 cpw 4536 {csn 4562 ⟨cop 4568 ∪ cuni 4845 ∪ ciun 4928 ↦ cmpt 5160 × cxp 5623 ^◡ccnv 5624 ran crn 5626 ↾ cres 5627 “ cima 5628 Rel wrel 5630 ⟶wf 6488 ‘cfv 6492 (class class class)co 7363 1^st c1st 7936 2^nd c2nd 7937 0cc0 11036 1c1 11037 − cmin 11375 / cdiv 11805 ℕcn 12172 (,)cioo 13296 [,]cicc 13299 ...cfz 13459 ↾_t crest 17381 topGenctg 17398 Cn ccn 23214 Homeochmeo 23743 IIcii 24867 CovMap ccvm 35490

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pr 5369 ax-un 7685

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-fv 6500 df-1st 7938 df-2nd 7939

This theorem is referenced by: cvmliftlem6 35525 cvmliftlem8 35527 cvmliftlem9 35528

W3C validator