Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftmolem1 Structured version   Visualization version   GIF version
Theorem cvmliftmolem1 34260
Description: Lemma for cvmliftmo 34263. (Contributed by Mario Carneiro, 10-Mar-2015.)
Hypotheses
Ref Expression
cvmliftmo.b 𝐡 = βˆͺ 𝐢
cvmliftmo.y π‘Œ = βˆͺ 𝐾
cvmliftmo.f (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
cvmliftmo.k (πœ‘ β†’ 𝐾 ∈ Conn)
cvmliftmo.l (πœ‘ β†’ 𝐾 ∈ 𝑛-Locally Conn)
cvmliftmo.o (πœ‘ β†’ 𝑂 ∈ π‘Œ)
cvmliftmoi.m (πœ‘ β†’ 𝑀 ∈ (𝐾 Cn 𝐢))
cvmliftmoi.n (πœ‘ β†’ 𝑁 ∈ (𝐾 Cn 𝐢))
cvmliftmoi.g (πœ‘ β†’ (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
cvmliftmoi.p (πœ‘ β†’ (π‘€β€˜π‘‚) = (π‘β€˜π‘‚))
cvmliftmolem.1 𝑆 = (π‘˜ ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑠 = (◑𝐹 β€œ π‘˜) ∧ βˆ€π‘’ ∈ 𝑠 (βˆ€π‘£ ∈ (𝑠 βˆ– {𝑒})(𝑒 ∩ 𝑣) = βˆ… ∧ (𝐹 β†Ύ 𝑒) ∈ ((𝐢 β†Ύt 𝑒)Homeo(𝐽 β†Ύt π‘˜))))})
cvmliftmolem.2 ((πœ‘ ∧ πœ“) β†’ 𝑇 ∈ (π‘†β€˜π‘ˆ))
cvmliftmolem.3 ((πœ‘ ∧ πœ“) β†’ π‘Š ∈ 𝑇)
cvmliftmolem.4 ((πœ‘ ∧ πœ“) β†’ 𝐼 βŠ† (◑𝑀 β€œ π‘Š))
cvmliftmolem.5 ((πœ‘ ∧ πœ“) β†’ (𝐾 β†Ύt 𝐼) ∈ Conn)
cvmliftmolem.6 ((πœ‘ ∧ πœ“) β†’ 𝑋 ∈ 𝐼)
cvmliftmolem.7 ((πœ‘ ∧ πœ“) β†’ 𝑄 ∈ 𝐼)
cvmliftmolem.8 ((πœ‘ ∧ πœ“) β†’ 𝑅 ∈ 𝐼)
cvmliftmolem.9 ((πœ‘ ∧ πœ“) β†’ (πΉβ€˜(π‘€β€˜π‘‹)) ∈ π‘ˆ)
Assertion
Ref Expression
cvmliftmolem1 ((πœ‘ ∧ πœ“) β†’ (𝑄 ∈ dom (𝑀 ∩ 𝑁) β†’ 𝑅 ∈ dom (𝑀 ∩ 𝑁)))
Distinct variable groups:   π‘˜,𝑠,𝑒,𝑣,𝐢   π‘˜,𝐽,𝑠,𝑒,𝑣   𝑣,𝐡   𝐾,𝑠   π‘˜,𝑀,𝑠,𝑒,𝑣   𝑁,𝑠   πœ‘,𝑠   π‘˜,𝐹,𝑠,𝑒,𝑣   𝑆,𝑠   π‘ˆ,π‘˜,𝑠,𝑒,𝑣   𝑇,𝑠,𝑒,𝑣   𝑒,π‘Š,𝑣   π‘Œ,𝑠
Allowed substitution hints:   πœ‘(𝑣,𝑒,π‘˜)   πœ“(𝑣,𝑒,π‘˜,𝑠)   𝐡(𝑒,π‘˜,𝑠)   𝑄(𝑣,𝑒,π‘˜,𝑠)   𝑅(𝑣,𝑒,π‘˜,𝑠)   𝑆(𝑣,𝑒,π‘˜)   𝑇(π‘˜)   𝐼(𝑣,𝑒,π‘˜,𝑠)   𝐾(𝑣,𝑒,π‘˜)   𝑁(𝑣,𝑒,π‘˜)   𝑂(𝑣,𝑒,π‘˜,𝑠)   π‘Š(π‘˜,𝑠)   𝑋(𝑣,𝑒,π‘˜,𝑠)   π‘Œ(𝑣,𝑒,π‘˜)
Proof of Theorem cvmliftmolem1
Dummy variable π‘₯ is distinct from all other variables.
StepHypRef Expression
1 cvmliftmoi.g . . . . . . . . . 10 (πœ‘ β†’ (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
21adantr 481 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
32fveq1d 6890 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ ((𝐹 ∘ 𝑀)β€˜π‘…) = ((𝐹 ∘ 𝑁)β€˜π‘…))
4 cvmliftmolem.4 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ 𝐼 βŠ† (◑𝑀 β€œ π‘Š))
5 cvmliftmolem.8 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ 𝑅 ∈ 𝐼)
64, 5sseldd 3982 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝑅 ∈ (◑𝑀 β€œ π‘Š))
7 cvmliftmoi.m . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 ∈ (𝐾 Cn 𝐢))
8 cvmliftmo.y . . . . . . . . . . . . . . 15 π‘Œ = βˆͺ 𝐾
9 cvmliftmo.b . . . . . . . . . . . . . . 15 𝐡 = βˆͺ 𝐢
108, 9cnf 22741 . . . . . . . . . . . . . 14 (𝑀 ∈ (𝐾 Cn 𝐢) β†’ 𝑀:π‘ŒβŸΆπ΅)
117, 10syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀:π‘ŒβŸΆπ΅)
1211ffnd 6715 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑀 Fn π‘Œ)
13 elpreima 7056 . . . . . . . . . . . 12 (𝑀 Fn π‘Œ β†’ (𝑅 ∈ (◑𝑀 β€œ π‘Š) ↔ (𝑅 ∈ π‘Œ ∧ (π‘€β€˜π‘…) ∈ π‘Š)))
1412, 13syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (𝑅 ∈ (◑𝑀 β€œ π‘Š) ↔ (𝑅 ∈ π‘Œ ∧ (π‘€β€˜π‘…) ∈ π‘Š)))
1514simprbda 499 . . . . . . . . . 10 ((πœ‘ ∧ 𝑅 ∈ (◑𝑀 β€œ π‘Š)) β†’ 𝑅 ∈ π‘Œ)
166, 15syldan 591 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ 𝑅 ∈ π‘Œ)
17 fvco3 6987 . . . . . . . . . 10 ((𝑀:π‘ŒβŸΆπ΅ ∧ 𝑅 ∈ π‘Œ) β†’ ((𝐹 ∘ 𝑀)β€˜π‘…) = (πΉβ€˜(π‘€β€˜π‘…)))
1811, 17sylan 580 . . . . . . . . 9 ((πœ‘ ∧ 𝑅 ∈ π‘Œ) β†’ ((𝐹 ∘ 𝑀)β€˜π‘…) = (πΉβ€˜(π‘€β€˜π‘…)))
1916, 18syldan 591 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ ((𝐹 ∘ 𝑀)β€˜π‘…) = (πΉβ€˜(π‘€β€˜π‘…)))
20 cvmliftmoi.n . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ (𝐾 Cn 𝐢))
218, 9cnf 22741 . . . . . . . . . . 11 (𝑁 ∈ (𝐾 Cn 𝐢) β†’ 𝑁:π‘ŒβŸΆπ΅)
2220, 21syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑁:π‘ŒβŸΆπ΅)
23 fvco3 6987 . . . . . . . . . 10 ((𝑁:π‘ŒβŸΆπ΅ ∧ 𝑅 ∈ π‘Œ) β†’ ((𝐹 ∘ 𝑁)β€˜π‘…) = (πΉβ€˜(π‘β€˜π‘…)))
2422, 23sylan 580 . . . . . . . . 9 ((πœ‘ ∧ 𝑅 ∈ π‘Œ) β†’ ((𝐹 ∘ 𝑁)β€˜π‘…) = (πΉβ€˜(π‘β€˜π‘…)))
2516, 24syldan 591 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ ((𝐹 ∘ 𝑁)β€˜π‘…) = (πΉβ€˜(π‘β€˜π‘…)))
263, 19, 253eqtr3d 2780 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ (πΉβ€˜(π‘€β€˜π‘…)) = (πΉβ€˜(π‘β€˜π‘…)))
2726adantr 481 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (πΉβ€˜(π‘€β€˜π‘…)) = (πΉβ€˜(π‘β€˜π‘…)))
2814simplbda 500 . . . . . . . . 9 ((πœ‘ ∧ 𝑅 ∈ (◑𝑀 β€œ π‘Š)) β†’ (π‘€β€˜π‘…) ∈ π‘Š)
296, 28syldan 591 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ (π‘€β€˜π‘…) ∈ π‘Š)
3029adantr 481 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (π‘€β€˜π‘…) ∈ π‘Š)
31 fvres 6907 . . . . . . 7 ((π‘€β€˜π‘…) ∈ π‘Š β†’ ((𝐹 β†Ύ π‘Š)β€˜(π‘€β€˜π‘…)) = (πΉβ€˜(π‘€β€˜π‘…)))
3230, 31syl 17 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝐹 β†Ύ π‘Š)β€˜(π‘€β€˜π‘…)) = (πΉβ€˜(π‘€β€˜π‘…)))
335adantr 481 . . . . . . . . 9 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ 𝑅 ∈ 𝐼)
34 fvres 6907 . . . . . . . . 9 (𝑅 ∈ 𝐼 β†’ ((𝑁 β†Ύ 𝐼)β€˜π‘…) = (π‘β€˜π‘…))
3533, 34syl 17 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝑁 β†Ύ 𝐼)β€˜π‘…) = (π‘β€˜π‘…))
36 eqid 2732 . . . . . . . . . . 11 βˆͺ (𝐾 β†Ύt 𝐼) = βˆͺ (𝐾 β†Ύt 𝐼)
37 cvmliftmolem.5 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (𝐾 β†Ύt 𝐼) ∈ Conn)
3837adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (𝐾 β†Ύt 𝐼) ∈ Conn)
3920adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝑁 ∈ (𝐾 Cn 𝐢))
40 cnvimass 6077 . . . . . . . . . . . . . . . . 17 (◑𝑀 β€œ π‘Š) βŠ† dom 𝑀
4140, 11fssdm 6734 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (◑𝑀 β€œ π‘Š) βŠ† π‘Œ)
4241adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ (◑𝑀 β€œ π‘Š) βŠ† π‘Œ)
434, 42sstrd 3991 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝐼 βŠ† π‘Œ)
448cnrest 22780 . . . . . . . . . . . . . 14 ((𝑁 ∈ (𝐾 Cn 𝐢) ∧ 𝐼 βŠ† π‘Œ) β†’ (𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn 𝐢))
4539, 43, 44syl2anc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ (𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn 𝐢))
46 cvmliftmo.f . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
4746adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ“) β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
48 cvmtop1 34239 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐢 ∈ Top)
4947, 48syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝐢 ∈ Top)
509toptopon 22410 . . . . . . . . . . . . . . 15 (𝐢 ∈ Top ↔ 𝐢 ∈ (TopOnβ€˜π΅))
5149, 50sylib 217 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝐢 ∈ (TopOnβ€˜π΅))
52 df-ima 5688 . . . . . . . . . . . . . . 15 (𝑁 β€œ 𝐼) = ran (𝑁 β†Ύ 𝐼)
53 cvmliftmolem.3 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ πœ“) β†’ π‘Š ∈ 𝑇)
54 elssuni 4940 . . . . . . . . . . . . . . . . . . . . 21 (π‘Š ∈ 𝑇 β†’ π‘Š βŠ† βˆͺ 𝑇)
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ“) β†’ π‘Š βŠ† βˆͺ 𝑇)
56 cvmliftmolem.2 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ πœ“) β†’ 𝑇 ∈ (π‘†β€˜π‘ˆ))
57 cvmliftmolem.1 . . . . . . . . . . . . . . . . . . . . . 22 𝑆 = (π‘˜ ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑠 = (◑𝐹 β€œ π‘˜) ∧ βˆ€π‘’ ∈ 𝑠 (βˆ€π‘£ ∈ (𝑠 βˆ– {𝑒})(𝑒 ∩ 𝑣) = βˆ… ∧ (𝐹 β†Ύ 𝑒) ∈ ((𝐢 β†Ύt 𝑒)Homeo(𝐽 β†Ύt π‘˜))))})
5857cvmsuni 34248 . . . . . . . . . . . . . . . . . . . . 21 (𝑇 ∈ (π‘†β€˜π‘ˆ) β†’ βˆͺ 𝑇 = (◑𝐹 β€œ π‘ˆ))
5956, 58syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ“) β†’ βˆͺ 𝑇 = (◑𝐹 β€œ π‘ˆ))
6055, 59sseqtrd 4021 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ πœ“) β†’ π‘Š βŠ† (◑𝐹 β€œ π‘ˆ))
61 imass2 6098 . . . . . . . . . . . . . . . . . . 19 (π‘Š βŠ† (◑𝐹 β€œ π‘ˆ) β†’ (◑𝑀 β€œ π‘Š) βŠ† (◑𝑀 β€œ (◑𝐹 β€œ π‘ˆ)))
6260, 61syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ“) β†’ (◑𝑀 β€œ π‘Š) βŠ† (◑𝑀 β€œ (◑𝐹 β€œ π‘ˆ)))
634, 62sstrd 3991 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ 𝐼 βŠ† (◑𝑀 β€œ (◑𝐹 β€œ π‘ˆ)))
642cnveqd 5873 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ“) β†’ β—‘(𝐹 ∘ 𝑀) = β—‘(𝐹 ∘ 𝑁))
65 cnvco 5883 . . . . . . . . . . . . . . . . . . . 20 β—‘(𝐹 ∘ 𝑀) = (◑𝑀 ∘ ◑𝐹)
66 cnvco 5883 . . . . . . . . . . . . . . . . . . . 20 β—‘(𝐹 ∘ 𝑁) = (◑𝑁 ∘ ◑𝐹)
6764, 65, 663eqtr3g 2795 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ πœ“) β†’ (◑𝑀 ∘ ◑𝐹) = (◑𝑁 ∘ ◑𝐹))
6867imaeq1d 6056 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ“) β†’ ((◑𝑀 ∘ ◑𝐹) β€œ π‘ˆ) = ((◑𝑁 ∘ ◑𝐹) β€œ π‘ˆ))
69 imaco 6247 . . . . . . . . . . . . . . . . . 18 ((◑𝑀 ∘ ◑𝐹) β€œ π‘ˆ) = (◑𝑀 β€œ (◑𝐹 β€œ π‘ˆ))
70 imaco 6247 . . . . . . . . . . . . . . . . . 18 ((◑𝑁 ∘ ◑𝐹) β€œ π‘ˆ) = (◑𝑁 β€œ (◑𝐹 β€œ π‘ˆ))
7168, 69, 703eqtr3g 2795 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ (◑𝑀 β€œ (◑𝐹 β€œ π‘ˆ)) = (◑𝑁 β€œ (◑𝐹 β€œ π‘ˆ)))
7263, 71sseqtrd 4021 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ“) β†’ 𝐼 βŠ† (◑𝑁 β€œ (◑𝐹 β€œ π‘ˆ)))
7322adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ“) β†’ 𝑁:π‘ŒβŸΆπ΅)
7473ffund 6718 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ Fun 𝑁)
7573fdmd 6725 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ“) β†’ dom 𝑁 = π‘Œ)
7643, 75sseqtrrd 4022 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ 𝐼 βŠ† dom 𝑁)
77 funimass3 7052 . . . . . . . . . . . . . . . . 17 ((Fun 𝑁 ∧ 𝐼 βŠ† dom 𝑁) β†’ ((𝑁 β€œ 𝐼) βŠ† (◑𝐹 β€œ π‘ˆ) ↔ 𝐼 βŠ† (◑𝑁 β€œ (◑𝐹 β€œ π‘ˆ))))
7874, 76, 77syl2anc 584 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ“) β†’ ((𝑁 β€œ 𝐼) βŠ† (◑𝐹 β€œ π‘ˆ) ↔ 𝐼 βŠ† (◑𝑁 β€œ (◑𝐹 β€œ π‘ˆ))))
7972, 78mpbird 256 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ (𝑁 β€œ 𝐼) βŠ† (◑𝐹 β€œ π‘ˆ))
8052, 79eqsstrrid 4030 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ ran (𝑁 β†Ύ 𝐼) βŠ† (◑𝐹 β€œ π‘ˆ))
81 cnvimass 6077 . . . . . . . . . . . . . . 15 (◑𝐹 β€œ π‘ˆ) βŠ† dom 𝐹
82 cvmcn 34241 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐹 ∈ (𝐢 Cn 𝐽))
8346, 82syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (𝐢 Cn 𝐽))
84 eqid 2732 . . . . . . . . . . . . . . . . . . 19 βˆͺ 𝐽 = βˆͺ 𝐽
859, 84cnf 22741 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (𝐢 Cn 𝐽) β†’ 𝐹:𝐡⟢βˆͺ 𝐽)
8683, 85syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹:𝐡⟢βˆͺ 𝐽)
8786fdmd 6725 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ dom 𝐹 = 𝐡)
8887adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ dom 𝐹 = 𝐡)
8981, 88sseqtrid 4033 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ (◑𝐹 β€œ π‘ˆ) βŠ† 𝐡)
90 cnrest2 22781 . . . . . . . . . . . . . 14 ((𝐢 ∈ (TopOnβ€˜π΅) ∧ ran (𝑁 β†Ύ 𝐼) βŠ† (◑𝐹 β€œ π‘ˆ) ∧ (◑𝐹 β€œ π‘ˆ) βŠ† 𝐡) β†’ ((𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn 𝐢) ↔ (𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ)))))
9151, 80, 89, 90syl3anc 1371 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ ((𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn 𝐢) ↔ (𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ)))))
9245, 91mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ))))
9392adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (𝑁 β†Ύ 𝐼) ∈ ((𝐾 β†Ύt 𝐼) Cn (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ))))
94 df-ss 3964 . . . . . . . . . . . . . 14 (π‘Š βŠ† (◑𝐹 β€œ π‘ˆ) ↔ (π‘Š ∩ (◑𝐹 β€œ π‘ˆ)) = π‘Š)
9560, 94sylib 217 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ (π‘Š ∩ (◑𝐹 β€œ π‘ˆ)) = π‘Š)
969topopn 22399 . . . . . . . . . . . . . . . 16 (𝐢 ∈ Top β†’ 𝐡 ∈ 𝐢)
9749, 96syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝐡 ∈ 𝐢)
9897, 89ssexd 5323 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ (◑𝐹 β€œ π‘ˆ) ∈ V)
9957cvmsss 34246 . . . . . . . . . . . . . . . 16 (𝑇 ∈ (π‘†β€˜π‘ˆ) β†’ 𝑇 βŠ† 𝐢)
10056, 99syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝑇 βŠ† 𝐢)
101100, 53sseldd 3982 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ π‘Š ∈ 𝐢)
102 elrestr 17370 . . . . . . . . . . . . . 14 ((𝐢 ∈ Top ∧ (◑𝐹 β€œ π‘ˆ) ∈ V ∧ π‘Š ∈ 𝐢) β†’ (π‘Š ∩ (◑𝐹 β€œ π‘ˆ)) ∈ (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ)))
10349, 98, 101, 102syl3anc 1371 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ (π‘Š ∩ (◑𝐹 β€œ π‘ˆ)) ∈ (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ)))
10495, 103eqeltrrd 2834 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ π‘Š ∈ (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ)))
105104adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ π‘Š ∈ (𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ)))
10657cvmscld 34252 . . . . . . . . . . . . 13 ((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑇 ∈ (π‘†β€˜π‘ˆ) ∧ π‘Š ∈ 𝑇) β†’ π‘Š ∈ (Clsdβ€˜(𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ))))
10747, 56, 53, 106syl3anc 1371 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ π‘Š ∈ (Clsdβ€˜(𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ))))
108107adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ π‘Š ∈ (Clsdβ€˜(𝐢 β†Ύt (◑𝐹 β€œ π‘ˆ))))
109 cvmliftmolem.7 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑄 ∈ 𝐼)
110 cvmliftmo.k . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐾 ∈ Conn)
111 conntop 22912 . . . . . . . . . . . . . . . 16 (𝐾 ∈ Conn β†’ 𝐾 ∈ Top)
112110, 111syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐾 ∈ Top)
113112adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝐾 ∈ Top)
1148restuni 22657 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝐼 βŠ† π‘Œ) β†’ 𝐼 = βˆͺ (𝐾 β†Ύt 𝐼))
115113, 43, 114syl2anc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝐼 = βˆͺ (𝐾 β†Ύt 𝐼))
116109, 115eleqtrd 2835 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ 𝑄 ∈ βˆͺ (𝐾 β†Ύt 𝐼))
117116adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ 𝑄 ∈ βˆͺ (𝐾 β†Ύt 𝐼))
118109adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ 𝑄 ∈ 𝐼)
119 fvres 6907 . . . . . . . . . . . . 13 (𝑄 ∈ 𝐼 β†’ ((𝑁 β†Ύ 𝐼)β€˜π‘„) = (π‘β€˜π‘„))
120118, 119syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝑁 β†Ύ 𝐼)β€˜π‘„) = (π‘β€˜π‘„))
121 simpr 485 . . . . . . . . . . . . 13 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (π‘€β€˜π‘„) = (π‘β€˜π‘„))
1224, 109sseldd 3982 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝑄 ∈ (◑𝑀 β€œ π‘Š))
123 elpreima 7056 . . . . . . . . . . . . . . . . 17 (𝑀 Fn π‘Œ β†’ (𝑄 ∈ (◑𝑀 β€œ π‘Š) ↔ (𝑄 ∈ π‘Œ ∧ (π‘€β€˜π‘„) ∈ π‘Š)))
12412, 123syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑄 ∈ (◑𝑀 β€œ π‘Š) ↔ (𝑄 ∈ π‘Œ ∧ (π‘€β€˜π‘„) ∈ π‘Š)))
125124simplbda 500 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑄 ∈ (◑𝑀 β€œ π‘Š)) β†’ (π‘€β€˜π‘„) ∈ π‘Š)
126122, 125syldan 591 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ (π‘€β€˜π‘„) ∈ π‘Š)
127126adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (π‘€β€˜π‘„) ∈ π‘Š)
128121, 127eqeltrrd 2834 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (π‘β€˜π‘„) ∈ π‘Š)
129120, 128eqeltrd 2833 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝑁 β†Ύ 𝐼)β€˜π‘„) ∈ π‘Š)
13036, 38, 93, 105, 108, 117, 129conncn 22921 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (𝑁 β†Ύ 𝐼):βˆͺ (𝐾 β†Ύt 𝐼)βŸΆπ‘Š)
131115adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ 𝐼 = βˆͺ (𝐾 β†Ύt 𝐼))
132131feq2d 6700 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝑁 β†Ύ 𝐼):πΌβŸΆπ‘Š ↔ (𝑁 β†Ύ 𝐼):βˆͺ (𝐾 β†Ύt 𝐼)βŸΆπ‘Š))
133130, 132mpbird 256 . . . . . . . . 9 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (𝑁 β†Ύ 𝐼):πΌβŸΆπ‘Š)
134133, 33ffvelcdmd 7084 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝑁 β†Ύ 𝐼)β€˜π‘…) ∈ π‘Š)
13535, 134eqeltrrd 2834 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (π‘β€˜π‘…) ∈ π‘Š)
136 fvres 6907 . . . . . . 7 ((π‘β€˜π‘…) ∈ π‘Š β†’ ((𝐹 β†Ύ π‘Š)β€˜(π‘β€˜π‘…)) = (πΉβ€˜(π‘β€˜π‘…)))
137135, 136syl 17 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝐹 β†Ύ π‘Š)β€˜(π‘β€˜π‘…)) = (πΉβ€˜(π‘β€˜π‘…)))
13827, 32, 1373eqtr4d 2782 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ ((𝐹 β†Ύ π‘Š)β€˜(π‘€β€˜π‘…)) = ((𝐹 β†Ύ π‘Š)β€˜(π‘β€˜π‘…)))
13957cvmsf1o 34251 . . . . . . . . 9 ((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑇 ∈ (π‘†β€˜π‘ˆ) ∧ π‘Š ∈ 𝑇) β†’ (𝐹 β†Ύ π‘Š):π‘Šβ€“1-1-ontoβ†’π‘ˆ)
14047, 56, 53, 139syl3anc 1371 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ (𝐹 β†Ύ π‘Š):π‘Šβ€“1-1-ontoβ†’π‘ˆ)
141 f1of1 6829 . . . . . . . 8 ((𝐹 β†Ύ π‘Š):π‘Šβ€“1-1-ontoβ†’π‘ˆ β†’ (𝐹 β†Ύ π‘Š):π‘Šβ€“1-1β†’π‘ˆ)
142140, 141syl 17 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ (𝐹 β†Ύ π‘Š):π‘Šβ€“1-1β†’π‘ˆ)
143142adantr 481 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (𝐹 β†Ύ π‘Š):π‘Šβ€“1-1β†’π‘ˆ)
144 f1fveq 7257 . . . . . 6 (((𝐹 β†Ύ π‘Š):π‘Šβ€“1-1β†’π‘ˆ ∧ ((π‘€β€˜π‘…) ∈ π‘Š ∧ (π‘β€˜π‘…) ∈ π‘Š)) β†’ (((𝐹 β†Ύ π‘Š)β€˜(π‘€β€˜π‘…)) = ((𝐹 β†Ύ π‘Š)β€˜(π‘β€˜π‘…)) ↔ (π‘€β€˜π‘…) = (π‘β€˜π‘…)))
145143, 30, 135, 144syl12anc 835 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (((𝐹 β†Ύ π‘Š)β€˜(π‘€β€˜π‘…)) = ((𝐹 β†Ύ π‘Š)β€˜(π‘β€˜π‘…)) ↔ (π‘€β€˜π‘…) = (π‘β€˜π‘…)))
146138, 145mpbid 231 . . . 4 (((πœ‘ ∧ πœ“) ∧ (π‘€β€˜π‘„) = (π‘β€˜π‘„)) β†’ (π‘€β€˜π‘…) = (π‘β€˜π‘…))
147146ex 413 . . 3 ((πœ‘ ∧ πœ“) β†’ ((π‘€β€˜π‘„) = (π‘β€˜π‘„) β†’ (π‘€β€˜π‘…) = (π‘β€˜π‘…)))
148124simprbda 499 . . . . 5 ((πœ‘ ∧ 𝑄 ∈ (◑𝑀 β€œ π‘Š)) β†’ 𝑄 ∈ π‘Œ)
149122, 148syldan 591 . . . 4 ((πœ‘ ∧ πœ“) β†’ 𝑄 ∈ π‘Œ)
150 fveq2 6888 . . . . . 6 (π‘₯ = 𝑄 β†’ (π‘€β€˜π‘₯) = (π‘€β€˜π‘„))
151 fveq2 6888 . . . . . 6 (π‘₯ = 𝑄 β†’ (π‘β€˜π‘₯) = (π‘β€˜π‘„))
152150, 151eqeq12d 2748 . . . . 5 (π‘₯ = 𝑄 β†’ ((π‘€β€˜π‘₯) = (π‘β€˜π‘₯) ↔ (π‘€β€˜π‘„) = (π‘β€˜π‘„)))
153152elrab3 3683 . . . 4 (𝑄 ∈ π‘Œ β†’ (𝑄 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)} ↔ (π‘€β€˜π‘„) = (π‘β€˜π‘„)))
154149, 153syl 17 . . 3 ((πœ‘ ∧ πœ“) β†’ (𝑄 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)} ↔ (π‘€β€˜π‘„) = (π‘β€˜π‘„)))
155 fveq2 6888 . . . . . 6 (π‘₯ = 𝑅 β†’ (π‘€β€˜π‘₯) = (π‘€β€˜π‘…))
156 fveq2 6888 . . . . . 6 (π‘₯ = 𝑅 β†’ (π‘β€˜π‘₯) = (π‘β€˜π‘…))
157155, 156eqeq12d 2748 . . . . 5 (π‘₯ = 𝑅 β†’ ((π‘€β€˜π‘₯) = (π‘β€˜π‘₯) ↔ (π‘€β€˜π‘…) = (π‘β€˜π‘…)))
158157elrab3 3683 . . . 4 (𝑅 ∈ π‘Œ β†’ (𝑅 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)} ↔ (π‘€β€˜π‘…) = (π‘β€˜π‘…)))
15916, 158syl 17 . . 3 ((πœ‘ ∧ πœ“) β†’ (𝑅 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)} ↔ (π‘€β€˜π‘…) = (π‘β€˜π‘…)))
160147, 154, 1593imtr4d 293 . 2 ((πœ‘ ∧ πœ“) β†’ (𝑄 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)} β†’ 𝑅 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)}))
16122ffnd 6715 . . . . 5 (πœ‘ β†’ 𝑁 Fn π‘Œ)
162 fndmin 7043 . . . . 5 ((𝑀 Fn π‘Œ ∧ 𝑁 Fn π‘Œ) β†’ dom (𝑀 ∩ 𝑁) = {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)})
16312, 161, 162syl2anc 584 . . . 4 (πœ‘ β†’ dom (𝑀 ∩ 𝑁) = {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)})
164163adantr 481 . . 3 ((πœ‘ ∧ πœ“) β†’ dom (𝑀 ∩ 𝑁) = {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)})
165164eleq2d 2819 . 2 ((πœ‘ ∧ πœ“) β†’ (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)}))
166164eleq2d 2819 . 2 ((πœ‘ ∧ πœ“) β†’ (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {π‘₯ ∈ π‘Œ ∣ (π‘€β€˜π‘₯) = (π‘β€˜π‘₯)}))
167160, 165, 1663imtr4d 293 1 ((πœ‘ ∧ πœ“) β†’ (𝑄 ∈ dom (𝑀 ∩ 𝑁) β†’ 𝑅 ∈ dom (𝑀 ∩ 𝑁)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432  Vcvv 3474   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907   ↦ cmpt 5230  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   ∘ ccom 5679  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536  β€“1-1β†’wf1 6537  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7405   β†Ύt crest 17362  Topctop 22386  TopOnctopon 22403  Clsdccld 22511   Cn ccn 22719  Conncconn 22906  π‘›-Locally cnlly 22960  Homeochmeo 23248   CovMap ccvm 34234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-map 8818  df-en 8936  df-fin 8939  df-fi 9402  df-rest 17364  df-topgen 17385  df-top 22387  df-topon 22404  df-bases 22440  df-cld 22514  df-cn 22722  df-conn 22907  df-hmeo 23250  df-cvm 34235
This theorem is referenced by:  cvmliftmolem2  34261
  Copyright terms: Public domain W3C validator