Proof of Theorem cvmlift3lem6
Step | Hyp | Ref
| Expression |
1 | | cvmlift3lem6.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (II Cn 𝐾)) |
2 | | cvmlift3.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ SCon) |
3 | | scontop 30464 |
. . . . . . . 8
⊢ (𝐾 ∈ SCon → 𝐾 ∈ Top) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
5 | | cnrest2r 20901 |
. . . . . . 7
⊢ (𝐾 ∈ Top → (II Cn (𝐾 ↾t 𝑀)) ⊆ (II Cn 𝐾)) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → (II Cn (𝐾 ↾t 𝑀)) ⊆ (II Cn 𝐾)) |
7 | | cvmlift3lem6.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (II Cn (𝐾 ↾t 𝑀))) |
8 | 6, 7 | sseldd 3569 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (II Cn 𝐾)) |
9 | | cvmlift3lem6.1 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻‘𝑋))) |
10 | 9 | simp2d 1067 |
. . . . . 6
⊢ (𝜑 → (𝑄‘1) = 𝑋) |
11 | | cvmlift3lem6.2 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍)) |
12 | 11 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝑁‘0) = 𝑋) |
13 | 10, 12 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → (𝑄‘1) = (𝑁‘0)) |
14 | 1, 8, 13 | pcocn 22625 |
. . . 4
⊢ (𝜑 → (𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾)) |
15 | 1, 8 | pco0 22622 |
. . . . 5
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘0) = (𝑄‘0)) |
16 | 9 | simp1d 1066 |
. . . . 5
⊢ (𝜑 → (𝑄‘0) = 𝑂) |
17 | 15, 16 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂) |
18 | 1, 8 | pco1 22623 |
. . . . 5
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘1) = (𝑁‘1)) |
19 | 11 | simprd 478 |
. . . . 5
⊢ (𝜑 → (𝑁‘1) = 𝑍) |
20 | 18, 19 | eqtrd 2644 |
. . . 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 20880 |
. . . . . . . . . . . 12
⊢ ((𝑄 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽)) |
26 | 1, 24, 25 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽)) |
27 | | cvmlift3.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
28 | 16 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝑄‘0)) = (𝐺‘𝑂)) |
29 | | iiuni 22492 |
. . . . . . . . . . . . . . 15
⊢ (0[,]1) =
∪ II |
30 | | cvmlift3.y |
. . . . . . . . . . . . . . 15
⊢ 𝑌 = ∪
𝐾 |
31 | 29, 30 | cnf 20860 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (II Cn 𝐾) → 𝑄:(0[,]1)⟶𝑌) |
32 | 1, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄:(0[,]1)⟶𝑌) |
33 | | 0elunit 12161 |
. . . . . . . . . . . . 13
⊢ 0 ∈
(0[,]1) |
34 | | fvco3 6185 |
. . . . . . . . . . . . 13
⊢ ((𝑄:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) →
((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0))) |
35 | 32, 33, 34 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0))) |
36 | | cvmlift3.e |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) |
37 | 28, 35, 36 | 3eqtr4rd 2655 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ 𝑄)‘0)) |
38 | 21, 22, 23, 26, 27, 37 | cvmliftiota 30537 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄) ∧ (𝑅‘0) = 𝑃)) |
39 | 38 | simp2d 1067 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄)) |
40 | | cvmlift3lem6.i |
. . . . . . . . . . 11
⊢ 𝐼 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑁) ∧ (𝑔‘0) = (𝐻‘𝑋))) |
41 | | cnco 20880 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽)) |
42 | 8, 24, 41 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽)) |
43 | | cvmlift3.l |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
PCon) |
44 | | cvmlift3.o |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑂 ∈ 𝑌) |
45 | | cvmlift3.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) |
46 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem3 30557 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:𝑌⟶𝐵) |
47 | | cvmlift3lem7.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ⊆ (◡𝐺 “ 𝐴)) |
48 | | cnvimass 5404 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐺 “ 𝐴) ⊆ dom 𝐺 |
49 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝐽 =
∪ 𝐽 |
50 | 30, 49 | cnf 20860 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) |
51 | 24, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽) |
52 | | fdm 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝑌⟶∪ 𝐽 → dom 𝐺 = 𝑌) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐺 = 𝑌) |
54 | 48, 53 | syl5sseq 3616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐺 “ 𝐴) ⊆ 𝑌) |
55 | 47, 54 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ⊆ 𝑌) |
56 | | cvmlift3lem6.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝑀) |
57 | 55, 56 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑌) |
58 | 46, 57 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝐵) |
59 | 12 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝑁‘0)) = (𝐺‘𝑋)) |
60 | 29, 30 | cnf 20860 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (II Cn 𝐾) → 𝑁:(0[,]1)⟶𝑌) |
61 | 8, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑌) |
62 | | fvco3 6185 |
. . . . . . . . . . . . 13
⊢ ((𝑁:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) →
((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0))) |
63 | 61, 33, 62 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0))) |
64 | | fvco3 6185 |
. . . . . . . . . . . . . 14
⊢ ((𝐻:𝑌⟶𝐵 ∧ 𝑋 ∈ 𝑌) → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) |
65 | 46, 57, 64 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) |
66 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem5 30559 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) |
67 | 66 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐺‘𝑋)) |
68 | 65, 67 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = (𝐺‘𝑋)) |
69 | 59, 63, 68 | 3eqtr4rd 2655 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = ((𝐺 ∘ 𝑁)‘0)) |
70 | 21, 40, 23, 42, 58, 69 | cvmliftiota 30537 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁) ∧ (𝐼‘0) = (𝐻‘𝑋))) |
71 | 70 | simp2d 1067 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁)) |
72 | 39, 71 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘ 𝑅)(*𝑝‘𝐽)(𝐹 ∘ 𝐼)) = ((𝐺 ∘ 𝑄)(*𝑝‘𝐽)(𝐺 ∘ 𝑁))) |
73 | 38 | simp1d 1066 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (II Cn 𝐶)) |
74 | 70 | simp1d 1066 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐶)) |
75 | 9 | simp3d 1068 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅‘1) = (𝐻‘𝑋)) |
76 | 70 | simp3d 1068 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘0) = (𝐻‘𝑋)) |
77 | 75, 76 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅‘1) = (𝐼‘0)) |
78 | | cvmcn 30498 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
79 | 23, 78 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽)) |
80 | 73, 74, 77, 79 | copco 22626 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = ((𝐹 ∘ 𝑅)(*𝑝‘𝐽)(𝐹 ∘ 𝐼))) |
81 | 1, 8, 13, 24 | copco 22626 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) = ((𝐺 ∘ 𝑄)(*𝑝‘𝐽)(𝐺 ∘ 𝑁))) |
82 | 72, 80, 81 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))) |
83 | 73, 74 | pco0 22622 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘0) = (𝑅‘0)) |
84 | 38 | simp3d 1068 |
. . . . . . . 8
⊢ (𝜑 → (𝑅‘0) = 𝑃) |
85 | 83, 84 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) |
86 | 73, 74, 77 | pcocn 22625 |
. . . . . . . 8
⊢ (𝜑 → (𝑅(*𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶)) |
87 | | cnco 20880 |
. . . . . . . . . 10
⊢ (((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) |
88 | 14, 24, 87 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) |
89 | 17 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0)) = (𝐺‘𝑂)) |
90 | 29, 30 | cnf 20860 |
. . . . . . . . . . . 12
⊢ ((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) → (𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌) |
91 | 14, 90 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌) |
92 | | fvco3 6185 |
. . . . . . . . . . 11
⊢ (((𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0))) |
93 | 91, 33, 92 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0))) |
94 | 89, 93, 36 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0)) |
95 | 21 | cvmlift 30535 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) |
96 | 23, 88, 27, 94, 95 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) |
97 | | coeq2 5202 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼))) |
98 | 97 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ↔ (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)))) |
99 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (𝑔‘0) = ((𝑅(*𝑝‘𝐶)𝐼)‘0)) |
100 | 99 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → ((𝑔‘0) = 𝑃 ↔ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃)) |
101 | 98, 100 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃))) |
102 | 101 | riota2 6533 |
. . . . . . . 8
⊢ (((𝑅(*𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼))) |
103 | 86, 96, 102 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼))) |
104 | 82, 85, 103 | mpbi2and 958 |
. . . . . 6
⊢ (𝜑 → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼)) |
105 | 104 | fveq1d 6105 |
. . . . 5
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = ((𝑅(*𝑝‘𝐶)𝐼)‘1)) |
106 | 73, 74 | pco1 22623 |
. . . . 5
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘1) = (𝐼‘1)) |
107 | 105, 106 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) |
108 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝑓‘0) = ((𝑄(*𝑝‘𝐾)𝑁)‘0)) |
109 | 108 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝑓‘0) = 𝑂 ↔ ((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂)) |
110 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝑓‘1) = ((𝑄(*𝑝‘𝐾)𝑁)‘1)) |
111 | 110 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝑓‘1) = 𝑍 ↔ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍)) |
112 | | coeq2 5202 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝐺 ∘ 𝑓) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))) |
113 | 112 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)))) |
114 | 113 | anbi1d 737 |
. . . . . . . . 9
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))) |
115 | 114 | riotabidv 6513 |
. . . . . . . 8
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))) |
116 | 115 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1)) |
117 | 116 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1) ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) |
118 | 109, 111,
117 | 3anbi123d 1391 |
. . . . 5
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) ↔ (((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) |
119 | 118 | rspcev 3282 |
. . . 4
⊢ (((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ (((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) |
120 | 14, 17, 20, 107, 119 | syl13anc 1320 |
. . 3
⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) |
121 | | cvmlift3lem6.z |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑀) |
122 | 55, 121 | sseldd 3569 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑌) |
123 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem4 30558 |
. . . 4
⊢ ((𝜑 ∧ 𝑍 ∈ 𝑌) → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) |
124 | 122, 123 | mpdan 699 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) |
125 | 120, 124 | mpbird 246 |
. 2
⊢ (𝜑 → (𝐻‘𝑍) = (𝐼‘1)) |
126 | | iicon 22498 |
. . . . 5
⊢ II ∈
Con |
127 | 126 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
Con) |
128 | | cvmtop1 30496 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
129 | 23, 128 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Top) |
130 | 21 | toptopon 20548 |
. . . . . . 7
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
131 | 129, 130 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
132 | 71 | rneqd 5274 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝐹 ∘ 𝐼) = ran (𝐺 ∘ 𝑁)) |
133 | | rnco2 5559 |
. . . . . . . . 9
⊢ ran
(𝐹 ∘ 𝐼) = (𝐹 “ ran 𝐼) |
134 | | rnco2 5559 |
. . . . . . . . 9
⊢ ran
(𝐺 ∘ 𝑁) = (𝐺 “ ran 𝑁) |
135 | 132, 133,
134 | 3eqtr3g 2667 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ ran 𝐼) = (𝐺 “ ran 𝑁)) |
136 | | iitopon 22490 |
. . . . . . . . . . . . 13
⊢ II ∈
(TopOn‘(0[,]1)) |
137 | 136 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
138 | 30 | toptopon 20548 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
139 | 4, 138 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
140 | | resttopon 20775 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑀 ⊆ 𝑌) → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
141 | 139, 55, 140 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
142 | | cnf2 20863 |
. . . . . . . . . . . 12
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀) ∧ 𝑁 ∈ (II Cn (𝐾 ↾t 𝑀))) → 𝑁:(0[,]1)⟶𝑀) |
143 | 137, 141,
7, 142 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑀) |
144 | | frn 5966 |
. . . . . . . . . . 11
⊢ (𝑁:(0[,]1)⟶𝑀 → ran 𝑁 ⊆ 𝑀) |
145 | 143, 144 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑁 ⊆ 𝑀) |
146 | 145, 47 | sstrd 3578 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑁 ⊆ (◡𝐺 “ 𝐴)) |
147 | | ffun 5961 |
. . . . . . . . . . 11
⊢ (𝐺:𝑌⟶∪ 𝐽 → Fun 𝐺) |
148 | 51, 147 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐺) |
149 | 146, 48 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑁 ⊆ dom 𝐺) |
150 | | funimass3 6241 |
. . . . . . . . . 10
⊢ ((Fun
𝐺 ∧ ran 𝑁 ⊆ dom 𝐺) → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (◡𝐺 “ 𝐴))) |
151 | 148, 149,
150 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (◡𝐺 “ 𝐴))) |
152 | 146, 151 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 “ ran 𝑁) ⊆ 𝐴) |
153 | 135, 152 | eqsstrd 3602 |
. . . . . . 7
⊢ (𝜑 → (𝐹 “ ran 𝐼) ⊆ 𝐴) |
154 | 21, 49 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
155 | 79, 154 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽) |
156 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝐹:𝐵⟶∪ 𝐽 → Fun 𝐹) |
157 | 155, 156 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
158 | 29, 21 | cnf 20860 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (II Cn 𝐶) → 𝐼:(0[,]1)⟶𝐵) |
159 | 74, 158 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼:(0[,]1)⟶𝐵) |
160 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐼:(0[,]1)⟶𝐵 → ran 𝐼 ⊆ 𝐵) |
161 | 159, 160 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐼 ⊆ 𝐵) |
162 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵) |
163 | 155, 162 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐵) |
164 | 161, 163 | sseqtr4d 3605 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐼 ⊆ dom 𝐹) |
165 | | funimass3 6241 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐼 ⊆ dom 𝐹) → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (◡𝐹 “ 𝐴))) |
166 | 157, 164,
165 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (◡𝐹 “ 𝐴))) |
167 | 153, 166 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → ran 𝐼 ⊆ (◡𝐹 “ 𝐴)) |
168 | | cnvimass 5404 |
. . . . . . 7
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 |
169 | 168, 163 | syl5sseq 3616 |
. . . . . 6
⊢ (𝜑 → (◡𝐹 “ 𝐴) ⊆ 𝐵) |
170 | | cnrest2 20900 |
. . . . . 6
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran 𝐼 ⊆ (◡𝐹 “ 𝐴) ∧ (◡𝐹 “ 𝐴) ⊆ 𝐵) → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴))))) |
171 | 131, 167,
169, 170 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴))))) |
172 | 74, 171 | mpbid 221 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴)))) |
173 | | cvmlift3lem7.2 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) |
174 | | cvmlift3lem7.s |
. . . . . . . 8
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
175 | 174 | cvmsss 30503 |
. . . . . . 7
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝑇 ⊆ 𝐶) |
176 | 173, 175 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑇 ⊆ 𝐶) |
177 | | cvmlift3lem7.1 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴) |
178 | 68, 177 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) ∈ 𝐴) |
179 | | cvmlift3lem7.w |
. . . . . . . . 9
⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏) |
180 | 174, 21, 179 | cvmsiota 30513 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝐴) ∧ (𝐻‘𝑋) ∈ 𝐵 ∧ (𝐹‘(𝐻‘𝑋)) ∈ 𝐴)) → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) |
181 | 23, 173, 58, 178, 180 | syl13anc 1320 |
. . . . . . 7
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) |
182 | 181 | simpld 474 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝑇) |
183 | 176, 182 | sseldd 3569 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝐶) |
184 | | elssuni 4403 |
. . . . . . 7
⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇) |
185 | 182, 184 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇) |
186 | 174 | cvmsuni 30505 |
. . . . . . 7
⊢ (𝑇 ∈ (𝑆‘𝐴) → ∪ 𝑇 = (◡𝐹 “ 𝐴)) |
187 | 173, 186 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑇 =
(◡𝐹 “ 𝐴)) |
188 | 185, 187 | sseqtrd 3604 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ (◡𝐹 “ 𝐴)) |
189 | 174 | cvmsrcl 30500 |
. . . . . . . 8
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝐴 ∈ 𝐽) |
190 | 173, 189 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝐽) |
191 | | cnima 20879 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ 𝐶) |
192 | 79, 190, 191 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (◡𝐹 “ 𝐴) ∈ 𝐶) |
193 | | restopn2 20791 |
. . . . . 6
⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝐴) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝐴)))) |
194 | 129, 192,
193 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝐴)))) |
195 | 183, 188,
194 | mpbir2and 959 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴))) |
196 | 174 | cvmscld 30509 |
. . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝐴) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝐴)))) |
197 | 23, 173, 182, 196 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝐴)))) |
198 | 33 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]1)) |
199 | 181 | simprd 478 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝑊) |
200 | 76, 199 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (𝐼‘0) ∈ 𝑊) |
201 | 29, 127, 172, 195, 197, 198, 200 | concn 21039 |
. . 3
⊢ (𝜑 → 𝐼:(0[,]1)⟶𝑊) |
202 | | 1elunit 12162 |
. . 3
⊢ 1 ∈
(0[,]1) |
203 | | ffvelrn 6265 |
. . 3
⊢ ((𝐼:(0[,]1)⟶𝑊 ∧ 1 ∈ (0[,]1)) →
(𝐼‘1) ∈ 𝑊) |
204 | 201, 202,
203 | sylancl 693 |
. 2
⊢ (𝜑 → (𝐼‘1) ∈ 𝑊) |
205 | 125, 204 | eqeltrd 2688 |
1
⊢ (𝜑 → (𝐻‘𝑍) ∈ 𝑊) |