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

Theorem cvmlift3lem7 31015
 Description: Lemma for cvmlift3 31018. (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 𝑊 = (𝑏𝑇 (𝐻𝑋) ∈ 𝑏)
cvmlift3lem7.7 (𝜑 → (𝐾t 𝑀) ∈ PConn)
cvmlift3lem7.4 (𝜑𝑉𝐾)
cvmlift3lem7.5 (𝜑𝑉𝑀)
cvmlift3lem7.6 (𝜑𝑋𝑉)
Assertion
Ref Expression
cvmlift3lem7 (𝜑𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋))
Distinct variable groups:   𝑏,𝑐,𝑑,𝑓,𝑘,𝑠,𝑧,𝐴   𝑓,𝑔,𝑧,𝑏,𝑥   𝐽,𝑏   𝑔,𝑐,𝑥,𝐽,𝑑,𝑓,𝑘,𝑠   𝐹,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠   𝑥,𝑧,𝐹   𝑓,𝑀,𝑔,𝑥   𝐻,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝑆,𝑏,𝑓,𝑥   𝐵,𝑏,𝑑,𝑓,𝑔,𝑥,𝑧   𝑋,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝐺,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑥,𝑧   𝑇,𝑏,𝑐,𝑑,𝑠   𝐶,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠,𝑥,𝑧   𝜑,𝑓,𝑥   𝐾,𝑏,𝑐,𝑓,𝑔,𝑥,𝑧   𝑃,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝑂,𝑏,𝑐,𝑓,𝑔,𝑥,𝑧   𝑓,𝑌,𝑔,𝑥,𝑧   𝑊,𝑐,𝑑,𝑓,𝑥
Allowed substitution hints:   𝜑(𝑧,𝑔,𝑘,𝑠,𝑏,𝑐,𝑑)   𝐴(𝑥,𝑔)   𝐵(𝑘,𝑠,𝑐)   𝑃(𝑘,𝑠)   𝑆(𝑧,𝑔,𝑘,𝑠,𝑐,𝑑)   𝑇(𝑥,𝑧,𝑓,𝑔,𝑘)   𝐺(𝑠)   𝐻(𝑘,𝑠)   𝐽(𝑧)   𝐾(𝑘,𝑠,𝑑)   𝑀(𝑧,𝑘,𝑠,𝑏,𝑐,𝑑)   𝑂(𝑘,𝑠,𝑑)   𝑉(𝑥,𝑧,𝑓,𝑔,𝑘,𝑠,𝑏,𝑐,𝑑)   𝑊(𝑧,𝑔,𝑘,𝑠,𝑏)   𝑋(𝑘,𝑠)   𝑌(𝑘,𝑠,𝑏,𝑐,𝑑)

Proof of Theorem cvmlift3lem7
Dummy variables 𝑎 𝑦 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmlift3.b . . . 4 𝐵 = 𝐶
2 cvmlift3.y . . . 4 𝑌 = 𝐾
3 cvmlift3lem7.s . . . 4 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))})
4 cvmlift3.f . . . 4 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
5 cvmlift3.k . . . . 5 (𝜑𝐾 ∈ SConn)
6 cvmlift3.l . . . . 5 (𝜑𝐾 ∈ 𝑛-Locally PConn)
7 cvmlift3.o . . . . 5 (𝜑𝑂𝑌)
8 cvmlift3.g . . . . 5 (𝜑𝐺 ∈ (𝐾 Cn 𝐽))
9 cvmlift3.p . . . . 5 (𝜑𝑃𝐵)
10 cvmlift3.e . . . . 5 (𝜑 → (𝐹𝑃) = (𝐺𝑂))
11 cvmlift3.h . . . . 5 𝐻 = (𝑥𝑌 ↦ (𝑧𝐵𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))
121, 2, 4, 5, 6, 7, 8, 9, 10, 11cvmlift3lem3 31011 . . . 4 (𝜑𝐻:𝑌𝐵)
131, 2, 4, 5, 6, 7, 8, 9, 10, 11cvmlift3lem5 31013 . . . . 5 (𝜑 → (𝐹𝐻) = 𝐺)
1413, 8eqeltrd 2698 . . . 4 (𝜑 → (𝐹𝐻) ∈ (𝐾 Cn 𝐽))
15 sconntop 30918 . . . . 5 (𝐾 ∈ SConn → 𝐾 ∈ Top)
165, 15syl 17 . . . 4 (𝜑𝐾 ∈ Top)
17 cvmlift3lem7.3 . . . . . 6 (𝜑𝑀 ⊆ (𝐺𝐴))
18 cnvimass 5444 . . . . . . 7 (𝐺𝐴) ⊆ dom 𝐺
19 eqid 2621 . . . . . . . . 9 𝐽 = 𝐽
202, 19cnf 20960 . . . . . . . 8 (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌 𝐽)
21 fdm 6008 . . . . . . . 8 (𝐺:𝑌 𝐽 → dom 𝐺 = 𝑌)
228, 20, 213syl 18 . . . . . . 7 (𝜑 → dom 𝐺 = 𝑌)
2318, 22syl5sseq 3632 . . . . . 6 (𝜑 → (𝐺𝐴) ⊆ 𝑌)
2417, 23sstrd 3593 . . . . 5 (𝜑𝑀𝑌)
25 cvmlift3lem7.5 . . . . . 6 (𝜑𝑉𝑀)
26 cvmlift3lem7.6 . . . . . 6 (𝜑𝑋𝑉)
2725, 26sseldd 3584 . . . . 5 (𝜑𝑋𝑀)
2824, 27sseldd 3584 . . . 4 (𝜑𝑋𝑌)
29 cvmlift3lem7.2 . . . 4 (𝜑𝑇 ∈ (𝑆𝐴))
3012, 28ffvelrnd 6316 . . . . 5 (𝜑 → (𝐻𝑋) ∈ 𝐵)
31 fvco3 6232 . . . . . . . 8 ((𝐻:𝑌𝐵𝑋𝑌) → ((𝐹𝐻)‘𝑋) = (𝐹‘(𝐻𝑋)))
3212, 28, 31syl2anc 692 . . . . . . 7 (𝜑 → ((𝐹𝐻)‘𝑋) = (𝐹‘(𝐻𝑋)))
3313fveq1d 6150 . . . . . . 7 (𝜑 → ((𝐹𝐻)‘𝑋) = (𝐺𝑋))
3432, 33eqtr3d 2657 . . . . . 6 (𝜑 → (𝐹‘(𝐻𝑋)) = (𝐺𝑋))
35 cvmlift3lem7.1 . . . . . 6 (𝜑 → (𝐺𝑋) ∈ 𝐴)
3634, 35eqeltrd 2698 . . . . 5 (𝜑 → (𝐹‘(𝐻𝑋)) ∈ 𝐴)
37 cvmlift3lem7.w . . . . . 6 𝑊 = (𝑏𝑇 (𝐻𝑋) ∈ 𝑏)
383, 1, 37cvmsiota 30967 . . . . 5 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆𝐴) ∧ (𝐻𝑋) ∈ 𝐵 ∧ (𝐹‘(𝐻𝑋)) ∈ 𝐴)) → (𝑊𝑇 ∧ (𝐻𝑋) ∈ 𝑊))
394, 29, 30, 36, 38syl13anc 1325 . . . 4 (𝜑 → (𝑊𝑇 ∧ (𝐻𝑋) ∈ 𝑊))
40 eqid 2621 . . . . . . . . . . 11 (𝐻𝑋) = (𝐻𝑋)
411, 2, 4, 5, 6, 7, 8, 9, 10, 11cvmlift3lem4 31012 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → ((𝐻𝑋) = (𝐻𝑋) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻𝑋))))
4240, 41mpbii 223 . . . . . . . . . 10 ((𝜑𝑋𝑌) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻𝑋)))
4328, 42mpdan 701 . . . . . . . . 9 (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻𝑋)))
4443adantr 481 . . . . . . . 8 ((𝜑𝑦𝑀) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻𝑋)))
45 fveq1 6147 . . . . . . . . . . 11 (𝑓 = → (𝑓‘0) = (‘0))
4645eqeq1d 2623 . . . . . . . . . 10 (𝑓 = → ((𝑓‘0) = 𝑂 ↔ (‘0) = 𝑂))
47 fveq1 6147 . . . . . . . . . . 11 (𝑓 = → (𝑓‘1) = (‘1))
4847eqeq1d 2623 . . . . . . . . . 10 (𝑓 = → ((𝑓‘1) = 𝑋 ↔ (‘1) = 𝑋))
49 coeq2 5240 . . . . . . . . . . . . . . . 16 (𝑓 = → (𝐺𝑓) = (𝐺))
5049eqeq2d 2631 . . . . . . . . . . . . . . 15 (𝑓 = → ((𝐹𝑔) = (𝐺𝑓) ↔ (𝐹𝑔) = (𝐺)))
5150anbi1d 740 . . . . . . . . . . . . . 14 (𝑓 = → (((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹𝑔) = (𝐺) ∧ (𝑔‘0) = 𝑃)))
5251riotabidv 6567 . . . . . . . . . . . . 13 (𝑓 = → (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃)) = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺) ∧ (𝑔‘0) = 𝑃)))
53 coeq2 5240 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑔 → (𝐹𝑎) = (𝐹𝑔))
5453eqeq1d 2623 . . . . . . . . . . . . . . 15 (𝑎 = 𝑔 → ((𝐹𝑎) = (𝐺) ↔ (𝐹𝑔) = (𝐺)))
55 fveq1 6147 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑔 → (𝑎‘0) = (𝑔‘0))
5655eqeq1d 2623 . . . . . . . . . . . . . . 15 (𝑎 = 𝑔 → ((𝑎‘0) = 𝑃 ↔ (𝑔‘0) = 𝑃))
5754, 56anbi12d 746 . . . . . . . . . . . . . 14 (𝑎 = 𝑔 → (((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃) ↔ ((𝐹𝑔) = (𝐺) ∧ (𝑔‘0) = 𝑃)))
5857cbvriotav 6576 . . . . . . . . . . . . 13 (𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃)) = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺) ∧ (𝑔‘0) = 𝑃))
5952, 58syl6eqr 2673 . . . . . . . . . . . 12 (𝑓 = → (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃)) = (𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃)))
6059fveq1d 6150 . . . . . . . . . . 11 (𝑓 = → ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1))
6160eqeq1d 2623 . . . . . . . . . 10 (𝑓 = → (((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻𝑋) ↔ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)))
6246, 48, 613anbi123d 1396 . . . . . . . . 9 (𝑓 = → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻𝑋)) ↔ ((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋))))
6362cbvrexv 3160 . . . . . . . 8 (∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻𝑋)) ↔ ∃ ∈ (II Cn 𝐾)((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)))
6444, 63sylib 208 . . . . . . 7 ((𝜑𝑦𝑀) → ∃ ∈ (II Cn 𝐾)((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)))
65 cvmlift3lem7.7 . . . . . . . . 9 (𝜑 → (𝐾t 𝑀) ∈ PConn)
6665adantr 481 . . . . . . . 8 ((𝜑𝑦𝑀) → (𝐾t 𝑀) ∈ PConn)
672restuni 20876 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ 𝑀𝑌) → 𝑀 = (𝐾t 𝑀))
6816, 24, 67syl2anc 692 . . . . . . . . . 10 (𝜑𝑀 = (𝐾t 𝑀))
6927, 68eleqtrd 2700 . . . . . . . . 9 (𝜑𝑋 (𝐾t 𝑀))
7069adantr 481 . . . . . . . 8 ((𝜑𝑦𝑀) → 𝑋 (𝐾t 𝑀))
7168eleq2d 2684 . . . . . . . . 9 (𝜑 → (𝑦𝑀𝑦 (𝐾t 𝑀)))
7271biimpa 501 . . . . . . . 8 ((𝜑𝑦𝑀) → 𝑦 (𝐾t 𝑀))
73 eqid 2621 . . . . . . . . 9 (𝐾t 𝑀) = (𝐾t 𝑀)
7473pconncn 30914 . . . . . . . 8 (((𝐾t 𝑀) ∈ PConn ∧ 𝑋 (𝐾t 𝑀) ∧ 𝑦 (𝐾t 𝑀)) → ∃𝑛 ∈ (II Cn (𝐾t 𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))
7566, 70, 72, 74syl3anc 1323 . . . . . . 7 ((𝜑𝑦𝑀) → ∃𝑛 ∈ (II Cn (𝐾t 𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))
76 reeanv 3097 . . . . . . . 8 (∃ ∈ (II Cn 𝐾)∃𝑛 ∈ (II Cn (𝐾t 𝑀))(((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) ↔ (∃ ∈ (II Cn 𝐾)((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ∃𝑛 ∈ (II Cn (𝐾t 𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)))
774ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
785ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐾 ∈ SConn)
796ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐾 ∈ 𝑛-Locally PConn)
807ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑂𝑌)
818ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐺 ∈ (𝐾 Cn 𝐽))
829ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑃𝐵)
8310ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → (𝐹𝑃) = (𝐺𝑂))
8435ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → (𝐺𝑋) ∈ 𝐴)
8529ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑇 ∈ (𝑆𝐴))
8617ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑀 ⊆ (𝐺𝐴))
8727ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑋𝑀)
88 simpllr 798 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑦𝑀)
89 simplrl 799 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → ∈ (II Cn 𝐾))
90 simprl 793 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → ((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)))
91 simplrr 800 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑛 ∈ (II Cn (𝐾t 𝑀)))
92 simprr 795 . . . . . . . . . . 11 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))
9353eqeq1d 2623 . . . . . . . . . . . . 13 (𝑎 = 𝑔 → ((𝐹𝑎) = (𝐺𝑛) ↔ (𝐹𝑔) = (𝐺𝑛)))
9455eqeq1d 2623 . . . . . . . . . . . . 13 (𝑎 = 𝑔 → ((𝑎‘0) = (𝐻𝑋) ↔ (𝑔‘0) = (𝐻𝑋)))
9593, 94anbi12d 746 . . . . . . . . . . . 12 (𝑎 = 𝑔 → (((𝐹𝑎) = (𝐺𝑛) ∧ (𝑎‘0) = (𝐻𝑋)) ↔ ((𝐹𝑔) = (𝐺𝑛) ∧ (𝑔‘0) = (𝐻𝑋))))
9695cbvriotav 6576 . . . . . . . . . . 11 (𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺𝑛) ∧ (𝑎‘0) = (𝐻𝑋))) = (𝑔 ∈ (II Cn 𝐶)((𝐹𝑔) = (𝐺𝑛) ∧ (𝑔‘0) = (𝐻𝑋)))
971, 2, 77, 78, 79, 80, 81, 82, 83, 11, 3, 84, 85, 86, 37, 87, 88, 89, 58, 90, 91, 92, 96cvmlift3lem6 31014 . . . . . . . . . 10 ((((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) ∧ (((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → (𝐻𝑦) ∈ 𝑊)
9897ex 450 . . . . . . . . 9 (((𝜑𝑦𝑀) ∧ ( ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾t 𝑀)))) → ((((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) → (𝐻𝑦) ∈ 𝑊))
9998rexlimdvva 3031 . . . . . . . 8 ((𝜑𝑦𝑀) → (∃ ∈ (II Cn 𝐾)∃𝑛 ∈ (II Cn (𝐾t 𝑀))(((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) → (𝐻𝑦) ∈ 𝑊))
10076, 99syl5bir 233 . . . . . . 7 ((𝜑𝑦𝑀) → ((∃ ∈ (II Cn 𝐾)((‘0) = 𝑂 ∧ (‘1) = 𝑋 ∧ ((𝑎 ∈ (II Cn 𝐶)((𝐹𝑎) = (𝐺) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻𝑋)) ∧ ∃𝑛 ∈ (II Cn (𝐾t 𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) → (𝐻𝑦) ∈ 𝑊))
10164, 75, 100mp2and 714 . . . . . 6 ((𝜑𝑦𝑀) → (𝐻𝑦) ∈ 𝑊)
102101ralrimiva 2960 . . . . 5 (𝜑 → ∀𝑦𝑀 (𝐻𝑦) ∈ 𝑊)
103 ffun 6005 . . . . . . 7 (𝐻:𝑌𝐵 → Fun 𝐻)
10412, 103syl 17 . . . . . 6 (𝜑 → Fun 𝐻)
105 fdm 6008 . . . . . . . 8 (𝐻:𝑌𝐵 → dom 𝐻 = 𝑌)
10612, 105syl 17 . . . . . . 7 (𝜑 → dom 𝐻 = 𝑌)
10724, 106sseqtr4d 3621 . . . . . 6 (𝜑𝑀 ⊆ dom 𝐻)
108 funimass4 6204 . . . . . 6 ((Fun 𝐻𝑀 ⊆ dom 𝐻) → ((𝐻𝑀) ⊆ 𝑊 ↔ ∀𝑦𝑀 (𝐻𝑦) ∈ 𝑊))
109104, 107, 108syl2anc 692 . . . . 5 (𝜑 → ((𝐻𝑀) ⊆ 𝑊 ↔ ∀𝑦𝑀 (𝐻𝑦) ∈ 𝑊))
110102, 109mpbird 247 . . . 4 (𝜑 → (𝐻𝑀) ⊆ 𝑊)
1111, 2, 3, 4, 12, 14, 16, 28, 29, 39, 24, 110cvmlift2lem9a 30993 . . 3 (𝜑 → (𝐻𝑀) ∈ ((𝐾t 𝑀) Cn 𝐶))
11273cncnpi 20992 . . 3 (((𝐻𝑀) ∈ ((𝐾t 𝑀) Cn 𝐶) ∧ 𝑋 (𝐾t 𝑀)) → (𝐻𝑀) ∈ (((𝐾t 𝑀) CnP 𝐶)‘𝑋))
113111, 69, 112syl2anc 692 . 2 (𝜑 → (𝐻𝑀) ∈ (((𝐾t 𝑀) CnP 𝐶)‘𝑋))
114 cvmlift3lem7.4 . . . . 5 (𝜑𝑉𝐾)
1152ssntr 20772 . . . . 5 (((𝐾 ∈ Top ∧ 𝑀𝑌) ∧ (𝑉𝐾𝑉𝑀)) → 𝑉 ⊆ ((int‘𝐾)‘𝑀))
11616, 24, 114, 25, 115syl22anc 1324 . . . 4 (𝜑𝑉 ⊆ ((int‘𝐾)‘𝑀))
117116, 26sseldd 3584 . . 3 (𝜑𝑋 ∈ ((int‘𝐾)‘𝑀))
1182, 1cnprest 21003 . . 3 (((𝐾 ∈ Top ∧ 𝑀𝑌) ∧ (𝑋 ∈ ((int‘𝐾)‘𝑀) ∧ 𝐻:𝑌𝐵)) → (𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋) ↔ (𝐻𝑀) ∈ (((𝐾t 𝑀) CnP 𝐶)‘𝑋)))
11916, 24, 117, 12, 118syl22anc 1324 . 2 (𝜑 → (𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋) ↔ (𝐻𝑀) ∈ (((𝐾t 𝑀) CnP 𝐶)‘𝑋)))
120113, 119mpbird 247 1 (𝜑𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  {crab 2911   ∖ cdif 3552   ∩ cin 3554   ⊆ wss 3555  ∅c0 3891  𝒫 cpw 4130  {csn 4148  ∪ cuni 4402   ↦ cmpt 4673  ◡ccnv 5073  dom cdm 5074   ↾ cres 5076   “ cima 5077   ∘ ccom 5078  Fun wfun 5841  ⟶wf 5843  ‘cfv 5847  ℩crio 6564  (class class class)co 6604  0cc0 9880  1c1 9881   ↾t crest 16002  Topctop 20617  intcnt 20731   Cn ccn 20938   CnP ccnp 20939  𝑛-Locally cnlly 21178  Homeochmeo 21466  IIcii 22586  PConncpconn 30909  SConncsconn 30910   CovMap ccvm 30945 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-ec 7689  df-map 7804  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-sum 14351  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-prds 16029  df-xrs 16083  df-qtop 16088  df-imas 16089  df-xps 16091  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-cnfld 19666  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-cn 20941  df-cnp 20942  df-cmp 21100  df-conn 21125  df-lly 21179  df-nlly 21180  df-tx 21275  df-hmeo 21468  df-xms 22035  df-ms 22036  df-tms 22037  df-ii 22588  df-htpy 22677  df-phtpy 22678  df-phtpc 22699  df-pco 22713  df-pconn 30911  df-sconn 30912  df-cvm 30946 This theorem is referenced by:  cvmlift3lem8  31016
 Copyright terms: Public domain W3C validator