Step | Hyp | Ref
| Expression |
1 | | cvmlift2lem9a.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
2 | | cvmtop1 30496 |
. . . 4
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Top) |
4 | | cnrest2r 20901 |
. . 3
⊢ (𝐶 ∈ Top → ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ⊆ ((𝐾 ↾t 𝑀) Cn 𝐶)) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ⊆ ((𝐾 ↾t 𝑀) Cn 𝐶)) |
6 | | cvmlift2lem9a.h |
. . . . . 6
⊢ (𝜑 → 𝐻:𝑌⟶𝐵) |
7 | | ffn 5958 |
. . . . . 6
⊢ (𝐻:𝑌⟶𝐵 → 𝐻 Fn 𝑌) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐻 Fn 𝑌) |
9 | | cvmlift2lem9a.4 |
. . . . 5
⊢ (𝜑 → 𝑀 ⊆ 𝑌) |
10 | | fnssres 5918 |
. . . . 5
⊢ ((𝐻 Fn 𝑌 ∧ 𝑀 ⊆ 𝑌) → (𝐻 ↾ 𝑀) Fn 𝑀) |
11 | 8, 9, 10 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝑀) Fn 𝑀) |
12 | | df-ima 5051 |
. . . . 5
⊢ (𝐻 “ 𝑀) = ran (𝐻 ↾ 𝑀) |
13 | | cvmlift2lem9a.6 |
. . . . 5
⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊) |
14 | 12, 13 | syl5eqssr 3613 |
. . . 4
⊢ (𝜑 → ran (𝐻 ↾ 𝑀) ⊆ 𝑊) |
15 | | df-f 5808 |
. . . 4
⊢ ((𝐻 ↾ 𝑀):𝑀⟶𝑊 ↔ ((𝐻 ↾ 𝑀) Fn 𝑀 ∧ ran (𝐻 ↾ 𝑀) ⊆ 𝑊)) |
16 | 11, 14, 15 | sylanbrc 695 |
. . 3
⊢ (𝜑 → (𝐻 ↾ 𝑀):𝑀⟶𝑊) |
17 | | cvmlift2lem9a.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) |
18 | | cvmlift2lem9a.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) |
19 | 18 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ 𝑇) |
20 | | cvmlift2lem9a.s |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
21 | 20 | cvmsf1o 30508 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝐴) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴) |
22 | 1, 17, 19, 21 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴) |
24 | | f1of1 6049 |
. . . . . . . . 9
⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝐴 → (𝐹 ↾ 𝑊):𝑊–1-1→𝐴) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝐴) |
26 | | cvmlift2lem9a.b |
. . . . . . . . . . . 12
⊢ 𝐵 = ∪
𝐶 |
27 | 26 | toptopon 20548 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
28 | 3, 27 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
29 | 20 | cvmsss 30503 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝑇 ⊆ 𝐶) |
30 | 17, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ⊆ 𝐶) |
31 | 30, 19 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ 𝐶) |
32 | | toponss 20544 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ 𝑊 ∈ 𝐶) → 𝑊 ⊆ 𝐵) |
33 | 28, 31, 32 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ⊆ 𝐵) |
34 | | resttopon 20775 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ 𝑊 ⊆ 𝐵) → (𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊)) |
35 | 28, 33, 34 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊)) |
36 | | toponss 20544 |
. . . . . . . . 9
⊢ (((𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊) ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝑥 ⊆ 𝑊) |
37 | 35, 36 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝑥 ⊆ 𝑊) |
38 | | f1imacnv 6066 |
. . . . . . . 8
⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝐴 ∧ 𝑥 ⊆ 𝑊) → (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = 𝑥) |
39 | 25, 37, 38 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = 𝑥) |
40 | 39 | imaeq2d 5385 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥))) = (◡(𝐻 ↾ 𝑀) “ 𝑥)) |
41 | | imaco 5557 |
. . . . . . 7
⊢ ((◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = (◡(𝐻 ↾ 𝑀) “ (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
42 | | cnvco 5230 |
. . . . . . . . 9
⊢ ◡((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = (◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) |
43 | | cores 5555 |
. . . . . . . . . . . . 13
⊢ (ran
(𝐻 ↾ 𝑀) ⊆ 𝑊 → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = (𝐹 ∘ (𝐻 ↾ 𝑀))) |
44 | 14, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = (𝐹 ∘ (𝐻 ↾ 𝑀))) |
45 | | resco 5556 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∘ 𝐻) ↾ 𝑀) = (𝐹 ∘ (𝐻 ↾ 𝑀)) |
46 | 44, 45 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = ((𝐹 ∘ 𝐻) ↾ 𝑀)) |
47 | 46 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = ((𝐹 ∘ 𝐻) ↾ 𝑀)) |
48 | 47 | cnveqd 5220 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ◡((𝐹 ↾ 𝑊) ∘ (𝐻 ↾ 𝑀)) = ◡((𝐹 ∘ 𝐻) ↾ 𝑀)) |
49 | 42, 48 | syl5eqr 2658 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) = ◡((𝐹 ∘ 𝐻) ↾ 𝑀)) |
50 | 49 | imaeq1d 5384 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((◡(𝐻 ↾ 𝑀) ∘ ◡(𝐹 ↾ 𝑊)) “ ((𝐹 ↾ 𝑊) “ 𝑥)) = (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
51 | 41, 50 | syl5eqr 2658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ (◡(𝐹 ↾ 𝑊) “ ((𝐹 ↾ 𝑊) “ 𝑥))) = (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
52 | 40, 51 | eqtr3d 2646 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ 𝑥) = (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥))) |
53 | | cvmlift2lem9a.g |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽)) |
54 | | cvmlift2lem9a.y |
. . . . . . . . 9
⊢ 𝑌 = ∪
𝐾 |
55 | 54 | cnrest 20899 |
. . . . . . . 8
⊢ (((𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽) ∧ 𝑀 ⊆ 𝑌) → ((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽)) |
56 | 53, 9, 55 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽)) |
57 | 56 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽)) |
58 | | resima2 5352 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝑊 → ((𝐹 ↾ 𝑊) “ 𝑥) = (𝐹 “ 𝑥)) |
59 | 37, 58 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ↾ 𝑊) “ 𝑥) = (𝐹 “ 𝑥)) |
60 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
61 | | restopn2 20791 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Top ∧ 𝑊 ∈ 𝐶) → (𝑥 ∈ (𝐶 ↾t 𝑊) ↔ (𝑥 ∈ 𝐶 ∧ 𝑥 ⊆ 𝑊))) |
62 | 3, 31, 61 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐶 ↾t 𝑊) ↔ (𝑥 ∈ 𝐶 ∧ 𝑥 ⊆ 𝑊))) |
63 | 62 | simprbda 651 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → 𝑥 ∈ 𝐶) |
64 | | cvmopn 30516 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ 𝐶) → (𝐹 “ 𝑥) ∈ 𝐽) |
65 | 60, 63, 64 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (𝐹 “ 𝑥) ∈ 𝐽) |
66 | 59, 65 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → ((𝐹 ↾ 𝑊) “ 𝑥) ∈ 𝐽) |
67 | | cnima 20879 |
. . . . . 6
⊢ ((((𝐹 ∘ 𝐻) ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐽) ∧ ((𝐹 ↾ 𝑊) “ 𝑥) ∈ 𝐽) → (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥)) ∈ (𝐾 ↾t 𝑀)) |
68 | 57, 66, 67 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡((𝐹 ∘ 𝐻) ↾ 𝑀) “ ((𝐹 ↾ 𝑊) “ 𝑥)) ∈ (𝐾 ↾t 𝑀)) |
69 | 52, 68 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶 ↾t 𝑊)) → (◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)) |
70 | 69 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐶 ↾t 𝑊)(◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)) |
71 | | cvmlift2lem9a.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
72 | 54 | toptopon 20548 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
73 | 71, 72 | sylib 207 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
74 | | resttopon 20775 |
. . . . 5
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑀 ⊆ 𝑌) → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
75 | 73, 9, 74 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
76 | | iscn 20849 |
. . . 4
⊢ (((𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀) ∧ (𝐶 ↾t 𝑊) ∈ (TopOn‘𝑊)) → ((𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ↔ ((𝐻 ↾ 𝑀):𝑀⟶𝑊 ∧ ∀𝑥 ∈ (𝐶 ↾t 𝑊)(◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)))) |
77 | 75, 35, 76 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊)) ↔ ((𝐻 ↾ 𝑀):𝑀⟶𝑊 ∧ ∀𝑥 ∈ (𝐶 ↾t 𝑊)(◡(𝐻 ↾ 𝑀) “ 𝑥) ∈ (𝐾 ↾t 𝑀)))) |
78 | 16, 70, 77 | mpbir2and 959 |
. 2
⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn (𝐶 ↾t 𝑊))) |
79 | 5, 78 | sseldd 3569 |
1
⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶)) |