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

Theorem cvmlift3lem6 32579
 Description: Lemma for cvmlift3 32583. (Contributed by Mario Carneiro, 9-Jul-2015.)
Hypotheses
Ref Expression
cvmlift3.b 𝐵 = 𝐶
cvmlift3.y 𝑌 = 𝐾
cvmlift3.f (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
cvmlift3.k (𝜑𝐾 ∈ SConn)
cvmlift3.l (𝜑𝐾 ∈ 𝑛-Locally PConn)
cvmlift3.o (𝜑𝑂𝑌)
cvmlift3.g (𝜑𝐺 ∈ (𝐾 Cn 𝐽))
cvmlift3.p (𝜑𝑃𝐵)
cvmlift3.e (𝜑 → (𝐹𝑃) = (𝐺𝑂))
cvmlift3.h 𝐻 = (𝑥𝑌 ↦ (𝑧𝐵𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))
cvmlift3lem7.s 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))})
cvmlift3lem7.1 (𝜑 → (𝐺𝑋) ∈ 𝐴)
cvmlift3lem7.2 (𝜑𝑇 ∈ (𝑆𝐴))
cvmlift3lem7.3 (𝜑𝑀 ⊆ (𝐺𝐴))
cvmlift3lem7.w 𝑊 = (𝑏𝑇 (𝐻𝑋) ∈ 𝑏)
cvmlift3lem6.x (𝜑𝑋𝑀)
cvmlift3lem6.z (𝜑𝑍𝑀)
cvmlift3lem6.q (𝜑𝑄 ∈ (II Cn 𝐾))
cvmlift3lem6.r 𝑅 = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑄) ∧ (𝑔‘0) = 𝑃))
cvmlift3lem6.1 (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻𝑋)))
cvmlift3lem6.n (𝜑𝑁 ∈ (II Cn (𝐾t 𝑀)))
cvmlift3lem6.2 (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍))
cvmlift3lem6.i 𝐼 = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑁) ∧ (𝑔‘0) = (𝐻𝑋)))
Assertion
Ref Expression
cvmlift3lem6 (𝜑 → (𝐻𝑍) ∈ 𝑊)
Distinct variable groups:   𝑏,𝑐,𝑑,𝑓,𝑘,𝑠,𝑧,𝐴   𝑓,𝑔,𝐼,𝑧   𝑔,𝑏,𝑥,𝐽,𝑐,𝑑,𝑓,𝑘,𝑠   𝐹,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠   𝑥,𝑧,𝐹   𝑓,𝑀,𝑔,𝑥   𝑓,𝑁,𝑔   𝐻,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝑄,𝑓,𝑔   𝑆,𝑏,𝑓,𝑥   𝐵,𝑏,𝑑,𝑓,𝑔,𝑥,𝑧   𝑅,𝑔   𝑋,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝐺,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑥,𝑧   𝑇,𝑏,𝑐,𝑑,𝑠   𝑓,𝑍,𝑔,𝑥,𝑧   𝐶,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠,𝑥,𝑧   𝜑,𝑓,𝑥   𝐾,𝑏,𝑐,𝑓,𝑔,𝑥,𝑧   𝑃,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝑂,𝑏,𝑐,𝑓,𝑔,𝑥,𝑧   𝑓,𝑌,𝑔,𝑥,𝑧   𝑊,𝑐,𝑑,𝑓,𝑥
Allowed substitution hints:   𝜑(𝑧,𝑔,𝑘,𝑠,𝑏,𝑐,𝑑)   𝐴(𝑥,𝑔)   𝐵(𝑘,𝑠,𝑐)   𝑃(𝑘,𝑠)   𝑄(𝑥,𝑧,𝑘,𝑠,𝑏,𝑐,𝑑)   𝑅(𝑥,𝑧,𝑓,𝑘,𝑠,𝑏,𝑐,𝑑)   𝑆(𝑧,𝑔,𝑘,𝑠,𝑐,𝑑)   𝑇(𝑥,𝑧,𝑓,𝑔,𝑘)   𝐺(𝑠)   𝐻(𝑘,𝑠)   𝐼(𝑥,𝑘,𝑠,𝑏,𝑐,𝑑)   𝐽(𝑧)   𝐾(𝑘,𝑠,𝑑)   𝑀(𝑧,𝑘,𝑠,𝑏,𝑐,𝑑)   𝑁(𝑥,𝑧,𝑘,𝑠,𝑏,𝑐,𝑑)   𝑂(𝑘,𝑠,𝑑)   𝑊(𝑧,𝑔,𝑘,𝑠,𝑏)   𝑋(𝑘,𝑠)   𝑌(𝑘,𝑠,𝑏,𝑐,𝑑)   𝑍(𝑘,𝑠,𝑏,𝑐,𝑑)

Proof of Theorem cvmlift3lem6
StepHypRef Expression
1 cvmlift3lem6.q . . . . 5 (𝜑𝑄 ∈ (II Cn 𝐾))
2 cvmlift3.k . . . . . . . 8 (𝜑𝐾 ∈ SConn)
3 sconntop 32483 . . . . . . . 8 (𝐾 ∈ SConn → 𝐾 ∈ Top)
42, 3syl 17 . . . . . . 7 (𝜑𝐾 ∈ Top)
5 cnrest2r 21871 . . . . . . 7 (𝐾 ∈ Top → (II Cn (𝐾t 𝑀)) ⊆ (II Cn 𝐾))
64, 5syl 17 . . . . . 6 (𝜑 → (II Cn (𝐾t 𝑀)) ⊆ (II Cn 𝐾))
7 cvmlift3lem6.n . . . . . 6 (𝜑𝑁 ∈ (II Cn (𝐾t 𝑀)))
86, 7sseldd 3947 . . . . 5 (𝜑𝑁 ∈ (II Cn 𝐾))
9 cvmlift3lem6.1 . . . . . . 7 (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻𝑋)))
109simp2d 1139 . . . . . 6 (𝜑 → (𝑄‘1) = 𝑋)
11 cvmlift3lem6.2 . . . . . . 7 (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍))
1211simpld 497 . . . . . 6 (𝜑 → (𝑁‘0) = 𝑋)
1310, 12eqtr4d 2858 . . . . 5 (𝜑 → (𝑄‘1) = (𝑁‘0))
141, 8, 13pcocn 23601 . . . 4 (𝜑 → (𝑄(*𝑝𝐾)𝑁) ∈ (II Cn 𝐾))
151, 8pco0 23598 . . . . 5 (𝜑 → ((𝑄(*𝑝𝐾)𝑁)‘0) = (𝑄‘0))
169simp1d 1138 . . . . 5 (𝜑 → (𝑄‘0) = 𝑂)
1715, 16eqtrd 2855 . . . 4 (𝜑 → ((𝑄(*𝑝𝐾)𝑁)‘0) = 𝑂)
181, 8pco1 23599 . . . . 5 (𝜑 → ((𝑄(*𝑝𝐾)𝑁)‘1) = (𝑁‘1))
1911simprd 498 . . . . 5 (𝜑 → (𝑁‘1) = 𝑍)
2018, 19eqtrd 2855 . . . 4 (𝜑 → ((𝑄(*𝑝𝐾)𝑁)‘1) = 𝑍)
21 cvmlift3.b . . . . . . . . . . 11 𝐵 = 𝐶
22 cvmlift3lem6.r . . . . . . . . . . 11 𝑅 = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑄) ∧ (𝑔‘0) = 𝑃))
23 cvmlift3.f . . . . . . . . . . 11 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
24 cvmlift3.g . . . . . . . . . . . 12 (𝜑𝐺 ∈ (𝐾 Cn 𝐽))
25 cnco 21850 . . . . . . . . . . . 12 ((𝑄 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺𝑄) ∈ (II Cn 𝐽))
261, 24, 25syl2anc 586 . . . . . . . . . . 11 (𝜑 → (𝐺𝑄) ∈ (II Cn 𝐽))
27 cvmlift3.p . . . . . . . . . . 11 (𝜑𝑃𝐵)
2816fveq2d 6650 . . . . . . . . . . . 12 (𝜑 → (𝐺‘(𝑄‘0)) = (𝐺𝑂))
29 iiuni 23465 . . . . . . . . . . . . . . 15 (0[,]1) = II
30 cvmlift3.y . . . . . . . . . . . . . . 15 𝑌 = 𝐾
3129, 30cnf 21830 . . . . . . . . . . . . . 14 (𝑄 ∈ (II Cn 𝐾) → 𝑄:(0[,]1)⟶𝑌)
321, 31syl 17 . . . . . . . . . . . . 13 (𝜑𝑄:(0[,]1)⟶𝑌)
33 0elunit 12838 . . . . . . . . . . . . 13 0 ∈ (0[,]1)
34 fvco3 6736 . . . . . . . . . . . . 13 ((𝑄:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺𝑄)‘0) = (𝐺‘(𝑄‘0)))
3532, 33, 34sylancl 588 . . . . . . . . . . . 12 (𝜑 → ((𝐺𝑄)‘0) = (𝐺‘(𝑄‘0)))
36 cvmlift3.e . . . . . . . . . . . 12 (𝜑 → (𝐹𝑃) = (𝐺𝑂))
3728, 35, 363eqtr4rd 2866 . . . . . . . . . . 11 (𝜑 → (𝐹𝑃) = ((𝐺𝑄)‘0))
3821, 22, 23, 26, 27, 37cvmliftiota 32556 . . . . . . . . . 10 (𝜑 → (𝑅 ∈ (II Cn 𝐶) ∧ (𝐹𝑅) = (𝐺𝑄) ∧ (𝑅‘0) = 𝑃))
3938simp2d 1139 . . . . . . . . 9 (𝜑 → (𝐹𝑅) = (𝐺𝑄))
40 cvmlift3lem6.i . . . . . . . . . . 11 𝐼 = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑁) ∧ (𝑔‘0) = (𝐻𝑋)))
41 cnco 21850 . . . . . . . . . . . 12 ((𝑁 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺𝑁) ∈ (II Cn 𝐽))
428, 24, 41syl2anc 586 . . . . . . . . . . 11 (𝜑 → (𝐺𝑁) ∈ (II Cn 𝐽))
43 cvmlift3.l . . . . . . . . . . . . 13 (𝜑𝐾 ∈ 𝑛-Locally PConn)
44 cvmlift3.o . . . . . . . . . . . . 13 (𝜑𝑂𝑌)
45 cvmlift3.h . . . . . . . . . . . . 13 𝐻 = (𝑥𝑌 ↦ (𝑧𝐵𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))
4621, 30, 23, 2, 43, 44, 24, 27, 36, 45cvmlift3lem3 32576 . . . . . . . . . . . 12 (𝜑𝐻:𝑌𝐵)
47 cvmlift3lem7.3 . . . . . . . . . . . . . 14 (𝜑𝑀 ⊆ (𝐺𝐴))
48 cnvimass 5925 . . . . . . . . . . . . . . 15 (𝐺𝐴) ⊆ dom 𝐺
49 eqid 2820 . . . . . . . . . . . . . . . . 17 𝐽 = 𝐽
5030, 49cnf 21830 . . . . . . . . . . . . . . . 16 (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌 𝐽)
5124, 50syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐺:𝑌 𝐽)
5248, 51fssdm 6506 . . . . . . . . . . . . . 14 (𝜑 → (𝐺𝐴) ⊆ 𝑌)
5347, 52sstrd 3956 . . . . . . . . . . . . 13 (𝜑𝑀𝑌)
54 cvmlift3lem6.x . . . . . . . . . . . . 13 (𝜑𝑋𝑀)
5553, 54sseldd 3947 . . . . . . . . . . . 12 (𝜑𝑋𝑌)
5646, 55ffvelrnd 6828 . . . . . . . . . . 11 (𝜑 → (𝐻𝑋) ∈ 𝐵)
5712fveq2d 6650 . . . . . . . . . . . 12 (𝜑 → (𝐺‘(𝑁‘0)) = (𝐺𝑋))
5829, 30cnf 21830 . . . . . . . . . . . . . 14 (𝑁 ∈ (II Cn 𝐾) → 𝑁:(0[,]1)⟶𝑌)
598, 58syl 17 . . . . . . . . . . . . 13 (𝜑𝑁:(0[,]1)⟶𝑌)
60 fvco3 6736 . . . . . . . . . . . . 13 ((𝑁:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺𝑁)‘0) = (𝐺‘(𝑁‘0)))
6159, 33, 60sylancl 588 . . . . . . . . . . . 12 (𝜑 → ((𝐺𝑁)‘0) = (𝐺‘(𝑁‘0)))
62 fvco3 6736 . . . . . . . . . . . . . 14 ((𝐻:𝑌𝐵𝑋𝑌) → ((𝐹𝐻)‘𝑋) = (𝐹‘(𝐻𝑋)))
6346, 55, 62syl2anc 586 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻)‘𝑋) = (𝐹‘(𝐻𝑋)))
6421, 30, 23, 2, 43, 44, 24, 27, 36, 45cvmlift3lem5 32578 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐻) = 𝐺)
6564fveq1d 6648 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻)‘𝑋) = (𝐺𝑋))
6663, 65eqtr3d 2857 . . . . . . . . . . . 12 (𝜑 → (𝐹‘(𝐻𝑋)) = (𝐺𝑋))
6757, 61, 663eqtr4rd 2866 . . . . . . . . . . 11 (𝜑 → (𝐹‘(𝐻𝑋)) = ((𝐺𝑁)‘0))
6821, 40, 23, 42, 56, 67cvmliftiota 32556 . . . . . . . . . 10 (𝜑 → (𝐼 ∈ (II Cn 𝐶) ∧ (𝐹𝐼) = (𝐺𝑁) ∧ (𝐼‘0) = (𝐻𝑋)))
6968simp2d 1139 . . . . . . . . 9 (𝜑 → (𝐹𝐼) = (𝐺𝑁))
7039, 69oveq12d 7151 . . . . . . . 8 (𝜑 → ((𝐹𝑅)(*𝑝𝐽)(𝐹𝐼)) = ((𝐺𝑄)(*𝑝𝐽)(𝐺𝑁)))
7138simp1d 1138 . . . . . . . . 9 (𝜑𝑅 ∈ (II Cn 𝐶))
7268simp1d 1138 . . . . . . . . 9 (𝜑𝐼 ∈ (II Cn 𝐶))
739simp3d 1140 . . . . . . . . . 10 (𝜑 → (𝑅‘1) = (𝐻𝑋))
7468simp3d 1140 . . . . . . . . . 10 (𝜑 → (𝐼‘0) = (𝐻𝑋))
7573, 74eqtr4d 2858 . . . . . . . . 9 (𝜑 → (𝑅‘1) = (𝐼‘0))
76 cvmcn 32517 . . . . . . . . . 10 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
7723, 76syl 17 . . . . . . . . 9 (𝜑𝐹 ∈ (𝐶 Cn 𝐽))
7871, 72, 75, 77copco 23602 . . . . . . . 8 (𝜑 → (𝐹 ∘ (𝑅(*𝑝𝐶)𝐼)) = ((𝐹𝑅)(*𝑝𝐽)(𝐹𝐼)))
791, 8, 13, 24copco 23602 . . . . . . . 8 (𝜑 → (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) = ((𝐺𝑄)(*𝑝𝐽)(𝐺𝑁)))
8070, 78, 793eqtr4d 2865 . . . . . . 7 (𝜑 → (𝐹 ∘ (𝑅(*𝑝𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)))
8171, 72pco0 23598 . . . . . . . 8 (𝜑 → ((𝑅(*𝑝𝐶)𝐼)‘0) = (𝑅‘0))
8238simp3d 1140 . . . . . . . 8 (𝜑 → (𝑅‘0) = 𝑃)
8381, 82eqtrd 2855 . . . . . . 7 (𝜑 → ((𝑅(*𝑝𝐶)𝐼)‘0) = 𝑃)
8471, 72, 75pcocn 23601 . . . . . . . 8 (𝜑 → (𝑅(*𝑝𝐶)𝐼) ∈ (II Cn 𝐶))
85 cnco 21850 . . . . . . . . . 10 (((𝑄(*𝑝𝐾)𝑁) ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∈ (II Cn 𝐽))
8614, 24, 85syl2anc 586 . . . . . . . . 9 (𝜑 → (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∈ (II Cn 𝐽))
8717fveq2d 6650 . . . . . . . . . 10 (𝜑 → (𝐺‘((𝑄(*𝑝𝐾)𝑁)‘0)) = (𝐺𝑂))
8829, 30cnf 21830 . . . . . . . . . . . 12 ((𝑄(*𝑝𝐾)𝑁) ∈ (II Cn 𝐾) → (𝑄(*𝑝𝐾)𝑁):(0[,]1)⟶𝑌)
8914, 88syl 17 . . . . . . . . . . 11 (𝜑 → (𝑄(*𝑝𝐾)𝑁):(0[,]1)⟶𝑌)
90 fvco3 6736 . . . . . . . . . . 11 (((𝑄(*𝑝𝐾)𝑁):(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺 ∘ (𝑄(*𝑝𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝𝐾)𝑁)‘0)))
9189, 33, 90sylancl 588 . . . . . . . . . 10 (𝜑 → ((𝐺 ∘ (𝑄(*𝑝𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝𝐾)𝑁)‘0)))
9287, 91, 363eqtr4rd 2866 . . . . . . . . 9 (𝜑 → (𝐹𝑃) = ((𝐺 ∘ (𝑄(*𝑝𝐾)𝑁))‘0))
9321cvmlift 32554 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∈ (II Cn 𝐽)) ∧ (𝑃𝐵 ∧ (𝐹𝑃) = ((𝐺 ∘ (𝑄(*𝑝𝐾)𝑁))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))
9423, 86, 27, 92, 93syl22anc 836 . . . . . . . 8 (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))
95 coeq2 5705 . . . . . . . . . . 11 (𝑔 = (𝑅(*𝑝𝐶)𝐼) → (𝐹𝑔) = (𝐹 ∘ (𝑅(*𝑝𝐶)𝐼)))
9695eqeq1d 2822 . . . . . . . . . 10 (𝑔 = (𝑅(*𝑝𝐶)𝐼) → ((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ↔ (𝐹 ∘ (𝑅(*𝑝𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁))))
97 fveq1 6645 . . . . . . . . . . 11 (𝑔 = (𝑅(*𝑝𝐶)𝐼) → (𝑔‘0) = ((𝑅(*𝑝𝐶)𝐼)‘0))
9897eqeq1d 2822 . . . . . . . . . 10 (𝑔 = (𝑅(*𝑝𝐶)𝐼) → ((𝑔‘0) = 𝑃 ↔ ((𝑅(*𝑝𝐶)𝐼)‘0) = 𝑃))
9996, 98anbi12d 632 . . . . . . . . 9 (𝑔 = (𝑅(*𝑝𝐶)𝐼) → (((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ (𝑅(*𝑝𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ ((𝑅(*𝑝𝐶)𝐼)‘0) = 𝑃)))
10099riota2 7116 . . . . . . . 8 (((𝑅(*𝑝𝐶)𝐼) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ (𝑅(*𝑝𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ ((𝑅(*𝑝𝐶)𝐼)‘0) = 𝑃) ↔ (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝𝐶)𝐼)))
10184, 94, 100syl2anc 586 . . . . . . 7 (𝜑 → (((𝐹 ∘ (𝑅(*𝑝𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ ((𝑅(*𝑝𝐶)𝐼)‘0) = 𝑃) ↔ (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝𝐶)𝐼)))
10280, 83, 101mpbi2and 710 . . . . . 6 (𝜑 → (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝𝐶)𝐼))
103102fveq1d 6648 . . . . 5 (𝜑 → ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = ((𝑅(*𝑝𝐶)𝐼)‘1))
10471, 72pco1 23599 . . . . 5 (𝜑 → ((𝑅(*𝑝𝐶)𝐼)‘1) = (𝐼‘1))
105103, 104eqtrd 2855 . . . 4 (𝜑 → ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))
106 fveq1 6645 . . . . . . 7 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → (𝑓‘0) = ((𝑄(*𝑝𝐾)𝑁)‘0))
107106eqeq1d 2822 . . . . . 6 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → ((𝑓‘0) = 𝑂 ↔ ((𝑄(*𝑝𝐾)𝑁)‘0) = 𝑂))
108 fveq1 6645 . . . . . . 7 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → (𝑓‘1) = ((𝑄(*𝑝𝐾)𝑁)‘1))
109108eqeq1d 2822 . . . . . 6 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → ((𝑓‘1) = 𝑍 ↔ ((𝑄(*𝑝𝐾)𝑁)‘1) = 𝑍))
110 coeq2 5705 . . . . . . . . . . 11 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → (𝐺𝑓) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)))
111110eqeq2d 2831 . . . . . . . . . 10 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → ((𝐹𝑔) = (𝐺𝑓) ↔ (𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁))))
112111anbi1d 631 . . . . . . . . 9 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → (((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)))
113112riotabidv 7093 . . . . . . . 8 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃)) = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)))
114113fveq1d 6648 . . . . . . 7 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1))
115114eqeq1d 2822 . . . . . 6 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → (((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1) ↔ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))
116107, 109, 1153anbi123d 1432 . . . . 5 (𝑓 = (𝑄(*𝑝𝐾)𝑁) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) ↔ (((𝑄(*𝑝𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝𝐾)𝑁)‘1) = 𝑍 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))))
117116rspcev 3602 . . . 4 (((𝑄(*𝑝𝐾)𝑁) ∈ (II Cn 𝐾) ∧ (((𝑄(*𝑝𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝𝐾)𝑁)‘1) = 𝑍 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺 ∘ (𝑄(*𝑝𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))
11814, 17, 20, 105, 117syl13anc 1368 . . 3 (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))
119 cvmlift3lem6.z . . . . 5 (𝜑𝑍𝑀)
12053, 119sseldd 3947 . . . 4 (𝜑𝑍𝑌)
12121, 30, 23, 2, 43, 44, 24, 27, 36, 45cvmlift3lem4 32577 . . . 4 ((𝜑𝑍𝑌) → ((𝐻𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))))
122120, 121mpdan 685 . . 3 (𝜑 → ((𝐻𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))))
123118, 122mpbird 259 . 2 (𝜑 → (𝐻𝑍) = (𝐼‘1))
124 iiconn 23471 . . . . 5 II ∈ Conn
125124a1i 11 . . . 4 (𝜑 → II ∈ Conn)
126 cvmtop1 32515 . . . . . . . 8 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
12723, 126syl 17 . . . . . . 7 (𝜑𝐶 ∈ Top)
12821toptopon 21501 . . . . . . 7 (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
129127, 128sylib 220 . . . . . 6 (𝜑𝐶 ∈ (TopOn‘𝐵))
13069rneqd 5784 . . . . . . . . 9 (𝜑 → ran (𝐹𝐼) = ran (𝐺𝑁))
131 rnco2 6082 . . . . . . . . 9 ran (𝐹𝐼) = (𝐹 “ ran 𝐼)
132 rnco2 6082 . . . . . . . . 9 ran (𝐺𝑁) = (𝐺 “ ran 𝑁)
133130, 131, 1323eqtr3g 2878 . . . . . . . 8 (𝜑 → (𝐹 “ ran 𝐼) = (𝐺 “ ran 𝑁))
134 iitopon 23463 . . . . . . . . . . . . 13 II ∈ (TopOn‘(0[,]1))
135134a1i 11 . . . . . . . . . . . 12 (𝜑 → II ∈ (TopOn‘(0[,]1)))
13630toptopon 21501 . . . . . . . . . . . . . 14 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
1374, 136sylib 220 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ (TopOn‘𝑌))
138 resttopon 21745 . . . . . . . . . . . . 13 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑀𝑌) → (𝐾t 𝑀) ∈ (TopOn‘𝑀))
139137, 53, 138syl2anc 586 . . . . . . . . . . . 12 (𝜑 → (𝐾t 𝑀) ∈ (TopOn‘𝑀))
140 cnf2 21833 . . . . . . . . . . . 12 ((II ∈ (TopOn‘(0[,]1)) ∧ (𝐾t 𝑀) ∈ (TopOn‘𝑀) ∧ 𝑁 ∈ (II Cn (𝐾t 𝑀))) → 𝑁:(0[,]1)⟶𝑀)
141135, 139, 7, 140syl3anc 1367 . . . . . . . . . . 11 (𝜑𝑁:(0[,]1)⟶𝑀)
142141frnd 6497 . . . . . . . . . 10 (𝜑 → ran 𝑁𝑀)
143142, 47sstrd 3956 . . . . . . . . 9 (𝜑 → ran 𝑁 ⊆ (𝐺𝐴))
14451ffund 6494 . . . . . . . . . 10 (𝜑 → Fun 𝐺)
145143, 48sstrdi 3958 . . . . . . . . . 10 (𝜑 → ran 𝑁 ⊆ dom 𝐺)
146 funimass3 6800 . . . . . . . . . 10 ((Fun 𝐺 ∧ ran 𝑁 ⊆ dom 𝐺) → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (𝐺𝐴)))
147144, 145, 146syl2anc 586 . . . . . . . . 9 (𝜑 → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (𝐺𝐴)))
148143, 147mpbird 259 . . . . . . . 8 (𝜑 → (𝐺 “ ran 𝑁) ⊆ 𝐴)
149133, 148eqsstrd 3984 . . . . . . 7 (𝜑 → (𝐹 “ ran 𝐼) ⊆ 𝐴)
15021, 49cnf 21830 . . . . . . . . . 10 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
15177, 150syl 17 . . . . . . . . 9 (𝜑𝐹:𝐵 𝐽)
152151ffund 6494 . . . . . . . 8 (𝜑 → Fun 𝐹)
15329, 21cnf 21830 . . . . . . . . . . 11 (𝐼 ∈ (II Cn 𝐶) → 𝐼:(0[,]1)⟶𝐵)
15472, 153syl 17 . . . . . . . . . 10 (𝜑𝐼:(0[,]1)⟶𝐵)
155154frnd 6497 . . . . . . . . 9 (𝜑 → ran 𝐼𝐵)
156151fdmd 6499 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐵)
157155, 156sseqtrrd 3987 . . . . . . . 8 (𝜑 → ran 𝐼 ⊆ dom 𝐹)
158 funimass3 6800 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐼 ⊆ dom 𝐹) → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (𝐹𝐴)))
159152, 157, 158syl2anc 586 . . . . . . 7 (𝜑 → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (𝐹𝐴)))
160149, 159mpbid 234 . . . . . 6 (𝜑 → ran 𝐼 ⊆ (𝐹𝐴))
161 cnvimass 5925 . . . . . . 7 (𝐹𝐴) ⊆ dom 𝐹
162161, 151fssdm 6506 . . . . . 6 (𝜑 → (𝐹𝐴) ⊆ 𝐵)
163 cnrest2 21870 . . . . . 6 ((𝐶 ∈ (TopOn‘𝐵) ∧ ran 𝐼 ⊆ (𝐹𝐴) ∧ (𝐹𝐴) ⊆ 𝐵) → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶t (𝐹𝐴)))))
164129, 160, 162, 163syl3anc 1367 . . . . 5 (𝜑 → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶t (𝐹𝐴)))))
16572, 164mpbid 234 . . . 4 (𝜑𝐼 ∈ (II Cn (𝐶t (𝐹𝐴))))
166 cvmlift3lem7.2 . . . . . . 7 (𝜑𝑇 ∈ (𝑆𝐴))
167 cvmlift3lem7.s . . . . . . . 8 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))})
168167cvmsss 32522 . . . . . . 7 (𝑇 ∈ (𝑆𝐴) → 𝑇𝐶)
169166, 168syl 17 . . . . . 6 (𝜑𝑇𝐶)
170 cvmlift3lem7.1 . . . . . . . . 9 (𝜑 → (𝐺𝑋) ∈ 𝐴)
17166, 170eqeltrd 2911 . . . . . . . 8 (𝜑 → (𝐹‘(𝐻𝑋)) ∈ 𝐴)
172 cvmlift3lem7.w . . . . . . . . 9 𝑊 = (𝑏𝑇 (𝐻𝑋) ∈ 𝑏)
173167, 21, 172cvmsiota 32532 . . . . . . . 8 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆𝐴) ∧ (𝐻𝑋) ∈ 𝐵 ∧ (𝐹‘(𝐻𝑋)) ∈ 𝐴)) → (𝑊𝑇 ∧ (𝐻𝑋) ∈ 𝑊))
17423, 166, 56, 171, 173syl13anc 1368 . . . . . . 7 (𝜑 → (𝑊𝑇 ∧ (𝐻𝑋) ∈ 𝑊))
175174simpld 497 . . . . . 6 (𝜑𝑊𝑇)
176169, 175sseldd 3947 . . . . 5 (𝜑𝑊𝐶)
177 elssuni 4844 . . . . . . 7 (𝑊𝑇𝑊 𝑇)
178175, 177syl 17 . . . . . 6 (𝜑𝑊 𝑇)
179167cvmsuni 32524 . . . . . . 7 (𝑇 ∈ (𝑆𝐴) → 𝑇 = (𝐹𝐴))
180166, 179syl 17 . . . . . 6 (𝜑 𝑇 = (𝐹𝐴))
181178, 180sseqtrd 3986 . . . . 5 (𝜑𝑊 ⊆ (𝐹𝐴))
182167cvmsrcl 32519 . . . . . . . 8 (𝑇 ∈ (𝑆𝐴) → 𝐴𝐽)
183166, 182syl 17 . . . . . . 7 (𝜑𝐴𝐽)
184 cnima 21849 . . . . . . 7 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝐴𝐽) → (𝐹𝐴) ∈ 𝐶)
18577, 183, 184syl2anc 586 . . . . . 6 (𝜑 → (𝐹𝐴) ∈ 𝐶)
186 restopn2 21761 . . . . . 6 ((𝐶 ∈ Top ∧ (𝐹𝐴) ∈ 𝐶) → (𝑊 ∈ (𝐶t (𝐹𝐴)) ↔ (𝑊𝐶𝑊 ⊆ (𝐹𝐴))))
187127, 185, 186syl2anc 586 . . . . 5 (𝜑 → (𝑊 ∈ (𝐶t (𝐹𝐴)) ↔ (𝑊𝐶𝑊 ⊆ (𝐹𝐴))))
188176, 181, 187mpbir2and 711 . . . 4 (𝜑𝑊 ∈ (𝐶t (𝐹𝐴)))
189167cvmscld 32528 . . . . 5 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆𝐴) ∧ 𝑊𝑇) → 𝑊 ∈ (Clsd‘(𝐶t (𝐹𝐴))))
19023, 166, 175, 189syl3anc 1367 . . . 4 (𝜑𝑊 ∈ (Clsd‘(𝐶t (𝐹𝐴))))
19133a1i 11 . . . 4 (𝜑 → 0 ∈ (0[,]1))
192174simprd 498 . . . . 5 (𝜑 → (𝐻𝑋) ∈ 𝑊)
19374, 192eqeltrd 2911 . . . 4 (𝜑 → (𝐼‘0) ∈ 𝑊)
19429, 125, 165, 188, 190, 191, 193conncn 22010 . . 3 (𝜑𝐼:(0[,]1)⟶𝑊)
195 1elunit 12839 . . 3 1 ∈ (0[,]1)
196 ffvelrn 6825 . . 3 ((𝐼:(0[,]1)⟶𝑊 ∧ 1 ∈ (0[,]1)) → (𝐼‘1) ∈ 𝑊)
197194, 195, 196sylancl 588 . 2 (𝜑 → (𝐼‘1) ∈ 𝑊)
198123, 197eqeltrd 2911 1 (𝜑 → (𝐻𝑍) ∈ 𝑊)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∀wral 3125  ∃wrex 3126  ∃!wreu 3127  {crab 3129   ∖ cdif 3910   ∩ cin 3912   ⊆ wss 3913  ∅c0 4269  𝒫 cpw 4515  {csn 4543  ∪ cuni 4814   ↦ cmpt 5122  ◡ccnv 5530  dom cdm 5531  ran crn 5532   ↾ cres 5533   “ cima 5534   ∘ ccom 5535  Fun wfun 6325  ⟶wf 6327  ‘cfv 6331  ℩crio 7090  (class class class)co 7133  0cc0 10515  1c1 10516  [,]cicc 12720   ↾t crest 16673  Topctop 21477  TopOnctopon 21494  Clsdccld 21600   Cn ccn 21808  Conncconn 21995  𝑛-Locally cnlly 22049  Homeochmeo 22337  IIcii 23459  *𝑝cpco 23584  PConncpconn 32474  SConncsconn 32475   CovMap ccvm 32510 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592  ax-pre-sup 10593  ax-addf 10594  ax-mulf 10595 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-iin 4898  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-of 7387  df-om 7559  df-1st 7667  df-2nd 7668  df-supp 7809  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-2o 8081  df-oadd 8084  df-er 8267  df-ec 8269  df-map 8386  df-ixp 8440  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-fsupp 8812  df-fi 8853  df-sup 8884  df-inf 8885  df-oi 8952  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-nn 11617  df-2 11679  df-3 11680  df-4 11681  df-5 11682  df-6 11683  df-7 11684  df-8 11685  df-9 11686  df-n0 11877  df-z 11961  df-dec 12078  df-uz 12223  df-q 12328  df-rp 12369  df-xneg 12486  df-xadd 12487  df-xmul 12488  df-ioo 12721  df-ico 12723  df-icc 12724  df-fz 12877  df-fzo 13018  df-fl 13146  df-seq 13354  df-exp 13415  df-hash 13676  df-cj 14438  df-re 14439  df-im 14440  df-sqrt 14574  df-abs 14575  df-clim 14825  df-sum 15023  df-struct 16464  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-mulr 16558  df-starv 16559  df-sca 16560  df-vsca 16561  df-ip 16562  df-tset 16563  df-ple 16564  df-ds 16566  df-unif 16567  df-hom 16568  df-cco 16569  df-rest 16675  df-topn 16676  df-0g 16694  df-gsum 16695  df-topgen 16696  df-pt 16697  df-prds 16700  df-xrs 16754  df-qtop 16759  df-imas 16760  df-xps 16762  df-mre 16836  df-mrc 16837  df-acs 16839  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-submnd 17936  df-mulg 18204  df-cntz 18426  df-cmn 18887  df-psmet 20513  df-xmet 20514  df-met 20515  df-bl 20516  df-mopn 20517  df-cnfld 20522  df-top 21478  df-topon 21495  df-topsp 21517  df-bases 21530  df-cld 21603  df-ntr 21604  df-cls 21605  df-nei 21682  df-cn 21811  df-cnp 21812  df-cmp 21971  df-conn 21996  df-lly 22050  df-nlly 22051  df-tx 22146  df-hmeo 22339  df-xms 22906  df-ms 22907  df-tms 22908  df-ii 23461  df-htpy 23554  df-phtpy 23555  df-phtpc 23576  df-pco 23589  df-pconn 32476  df-sconn 32477  df-cvm 32511 This theorem is referenced by:  cvmlift3lem7  32580
 Copyright terms: Public domain W3C validator