| Step | Hyp | Ref
| Expression |
| 1 | | cvmlift2lem9a.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 2 | | cvmtop1 35265 |
. . . 4
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Top) |
| 4 | | cnrest2r 23295 |
. . 3
⊢ (𝐶 ∈ Top → ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ⊆ ((𝐾 ↾t 𝑀) Cn 𝐶)) |
| 5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ⊆ ((𝐾 ↾t 𝑀) Cn 𝐶)) |
| 6 | | cvmlift2lem9a.h |
. . . . . 6
⊢ (𝜑 → 𝐻:𝑌⟶𝐵) |
| 7 | 6 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → 𝐻 Fn 𝑌) |
| 8 | | cvmlift2lem9a.4 |
. . . . 5
⊢ (𝜑 → 𝑀 ⊆ 𝑌) |
| 9 | | fnssres 6691 |
. . . . 5
⊢ ((𝐻 Fn 𝑌 ∧ 𝑀 ⊆ 𝑌) → (𝐻 ↾ 𝑀) Fn 𝑀) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝑀) Fn 𝑀) |
| 11 | | df-ima 5698 |
. . . . 5
⊢ (𝐻 “ 𝑀) = ran (𝐻 ↾ 𝑀) |
| 12 | | cvmlift2lem9a.6 |
. . . . 5
⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊) |
| 13 | 11, 12 | eqsstrrid 4023 |
. . . 4
⊢ (𝜑 → ran (𝐻 ↾ 𝑀) ⊆ 𝑊) |
| 14 | | df-f 6565 |
. . . 4
⊢ ((𝐻 ↾ 𝑀):𝑀⟶𝑊 ↔ ((𝐻 ↾ 𝑀) Fn 𝑀 ∧ ran (𝐻 ↾ 𝑀) ⊆ 𝑊)) |
| 15 | 10, 13, 14 | sylanbrc 583 |
. . 3
⊢ (𝜑 → (𝐻 ↾ 𝑀):𝑀⟶𝑊) |
| 16 | | cvmlift2lem9a.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) |
| 17 | | cvmlift2lem9a.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) |
| 18 | 17 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ 𝑇) |
| 19 | | cvmlift2lem9a.s |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
| 20 | 19 | cvmsf1o 35277 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝐴) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴) |
| 21 | 1, 16, 18, 20 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴) |
| 22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴) |
| 23 | | f1of1 6847 |
. . . . . . . . 9
⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴 → (𝐹 ↾ 𝑊):𝑊–1-1→𝐴) |
| 24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝐴) |
| 25 | | cvmlift2lem9a.b |
. . . . . . . . . . . 12
⊢ 𝐵 = ∪
𝐶 |
| 26 | 25 | toptopon 22923 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
| 27 | 3, 26 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
| 28 | 19 | cvmsss 35272 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝑇 ⊆ 𝐶) |
| 29 | 16, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ⊆ 𝐶) |
| 30 | 29, 18 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ 𝐶) |
| 31 | | toponss 22933 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ 𝑊 ∈ 𝐶) → 𝑊 ⊆ 𝐵) |
| 32 | 27, 30, 31 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ⊆ 𝐵) |
| 33 | | resttopon 23169 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ 𝑊 ⊆ 𝐵) → (𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊)) |
| 34 | 27, 32, 33 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊)) |
| 35 | | toponss 22933 |
. . . . . . . . 9
⊢ (((𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊) ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝑥 ⊆ 𝑊) |
| 36 | 34, 35 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝑥 ⊆ 𝑊) |
| 37 | | f1imacnv 6864 |
. . . . . . . 8
⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝐴 ∧ 𝑥 ⊆ 𝑊) → (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = 𝑥) |
| 38 | 24, 36, 37 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = 𝑥) |
| 39 | 38 | imaeq2d 6078 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥))) = (◡(𝐻 ↾ 𝑀) “ 𝑥)) |
| 40 | | imaco 6271 |
. . . . . . 7
⊢ ((◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = (◡(𝐻 ↾ 𝑀) “ (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
| 41 | | cnvco 5896 |
. . . . . . . . 9
⊢ ◡((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = (◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) |
| 42 | | cores 6269 |
. . . . . . . . . . . . 13
⊢ (ran
(𝐻 ↾ 𝑀) ⊆ 𝑊 → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = (𝐹 ∘ (𝐻 ↾ 𝑀))) |
| 43 | 13, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = (𝐹 ∘ (𝐻 ↾ 𝑀))) |
| 44 | | resco 6270 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∘ 𝐻) ↾ 𝑀) = (𝐹 ∘ (𝐻 ↾ 𝑀)) |
| 45 | 43, 44 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = ((𝐹 ∘ 𝐻) ↾ 𝑀)) |
| 46 | 45 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = ((𝐹 ∘ 𝐻) ↾ 𝑀)) |
| 47 | 46 | cnveqd 5886 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ◡((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = ◡((𝐹 ∘ 𝐻) ↾ 𝑀)) |
| 48 | 41, 47 | eqtr3id 2791 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) = ◡((𝐹 ∘ 𝐻) ↾ 𝑀)) |
| 49 | 48 | imaeq1d 6077 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
| 50 | 40, 49 | eqtr3id 2791 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥))) = (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
| 51 | 39, 50 | eqtr3d 2779 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ 𝑥) = (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
| 52 | | cvmlift2lem9a.g |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽)) |
| 53 | | cvmlift2lem9a.y |
. . . . . . . . 9
⊢ 𝑌 = ∪
𝐾 |
| 54 | 53 | cnrest 23293 |
. . . . . . . 8
⊢ (((𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽) ∧ 𝑀 ⊆ 𝑌) → ((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽)) |
| 55 | 52, 8, 54 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽)) |
| 56 | 55 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽)) |
| 57 | | resima2 6034 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝑊 → ((𝐹 ↾ 𝑊) “ 𝑥) = (𝐹 “ 𝑥)) |
| 58 | 36, 57 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ↾ 𝑊) “ 𝑥) = (𝐹 “ 𝑥)) |
| 59 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 60 | | restopn2 23185 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Top ∧ 𝑊 ∈ 𝐶) → (𝑥 ∈ (𝐶 ↾t 𝑊) ↔ (𝑥 ∈ 𝐶 ∧ 𝑥 ⊆ 𝑊))) |
| 61 | 3, 30, 60 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐶 ↾t 𝑊) ↔ (𝑥 ∈ 𝐶 ∧ 𝑥 ⊆ 𝑊))) |
| 62 | 61 | simprbda 498 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝑥 ∈ 𝐶) |
| 63 | | cvmopn 35285 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ 𝐶) → (𝐹 “ 𝑥) ∈ 𝐽) |
| 64 | 59, 62, 63 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (𝐹 “ 𝑥) ∈ 𝐽) |
| 65 | 58, 64 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ↾ 𝑊) “ 𝑥) ∈ 𝐽) |
| 66 | | cnima 23273 |
. . . . . 6
⊢ ((((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽) ∧ ((𝐹 ↾ 𝑊) “ 𝑥) ∈ 𝐽) → (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥)) ∈ (𝐾 ↾t 𝑀)) |
| 67 | 56, 65, 66 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥)) ∈ (𝐾 ↾t 𝑀)) |
| 68 | 51, 67 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)) |
| 69 | 68 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐶 ↾t 𝑊)(◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)) |
| 70 | | cvmlift2lem9a.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
| 71 | 53 | toptopon 22923 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
| 72 | 70, 71 | sylib 218 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
| 73 | | resttopon 23169 |
. . . . 5
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑀 ⊆ 𝑌) → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
| 74 | 72, 8, 73 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
| 75 | | iscn 23243 |
. . . 4
⊢ (((𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀) ∧ (𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊)) → ((𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ↔ ((𝐻 ↾ 𝑀):𝑀⟶𝑊 ∧ ∀𝑥 ∈ (𝐶 ↾t 𝑊)(◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)))) |
| 76 | 74, 34, 75 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ↔ ((𝐻 ↾ 𝑀):𝑀⟶𝑊 ∧ ∀𝑥 ∈ (𝐶 ↾t 𝑊)(◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)))) |
| 77 | 15, 69, 76 | mpbir2and 713 |
. 2
⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊))) |
| 78 | 5, 77 | sseldd 3984 |
1
⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶)) |