Proof of Theorem cvmlift3lem6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cvmlift3lem6.q | . . . . 5
⊢ (𝜑 → 𝑄 ∈ (II Cn 𝐾)) | 
| 2 |  | cvmlift3.k | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ SConn) | 
| 3 |  | sconntop 35234 | . . . . . . . 8
⊢ (𝐾 ∈ SConn → 𝐾 ∈ Top) | 
| 4 | 2, 3 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 5 |  | cnrest2r 23296 | . . . . . . 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 3983 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ (II Cn 𝐾)) | 
| 9 |  | cvmlift3lem6.1 | . . . . . . 7
⊢ (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻‘𝑋))) | 
| 10 | 9 | simp2d 1143 | . . . . . 6
⊢ (𝜑 → (𝑄‘1) = 𝑋) | 
| 11 |  | cvmlift3lem6.2 | . . . . . . 7
⊢ (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍)) | 
| 12 | 11 | simpld 494 | . . . . . 6
⊢ (𝜑 → (𝑁‘0) = 𝑋) | 
| 13 | 10, 12 | eqtr4d 2779 | . . . . 5
⊢ (𝜑 → (𝑄‘1) = (𝑁‘0)) | 
| 14 | 1, 8, 13 | pcocn 25051 | . . . 4
⊢ (𝜑 → (𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾)) | 
| 15 | 1, 8 | pco0 25048 | . . . . 5
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘0) = (𝑄‘0)) | 
| 16 | 9 | simp1d 1142 | . . . . 5
⊢ (𝜑 → (𝑄‘0) = 𝑂) | 
| 17 | 15, 16 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂) | 
| 18 | 1, 8 | pco1 25049 | . . . . 5
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘1) = (𝑁‘1)) | 
| 19 | 11 | simprd 495 | . . . . 5
⊢ (𝜑 → (𝑁‘1) = 𝑍) | 
| 20 | 18, 19 | eqtrd 2776 | . . . 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 23275 | . . . . . . . . . . . 12
⊢ ((𝑄 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽)) | 
| 26 | 1, 24, 25 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽)) | 
| 27 |  | cvmlift3.p | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ 𝐵) | 
| 28 | 16 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝑄‘0)) = (𝐺‘𝑂)) | 
| 29 |  | iiuni 24908 | . . . . . . . . . . . . . . 15
⊢ (0[,]1) =
∪ II | 
| 30 |  | cvmlift3.y | . . . . . . . . . . . . . . 15
⊢ 𝑌 = ∪
𝐾 | 
| 31 | 29, 30 | cnf 23255 | . . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (II Cn 𝐾) → 𝑄:(0[,]1)⟶𝑌) | 
| 32 | 1, 31 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄:(0[,]1)⟶𝑌) | 
| 33 |  | 0elunit 13510 | . . . . . . . . . . . . 13
⊢ 0 ∈
(0[,]1) | 
| 34 |  | fvco3 7007 | . . . . . . . . . . . . 13
⊢ ((𝑄:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) →
((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0))) | 
| 35 | 32, 33, 34 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0))) | 
| 36 |  | cvmlift3.e | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) | 
| 37 | 28, 35, 36 | 3eqtr4rd 2787 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ 𝑄)‘0)) | 
| 38 | 21, 22, 23, 26, 27, 37 | cvmliftiota 35307 | . . . . . . . . . 10
⊢ (𝜑 → (𝑅 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄) ∧ (𝑅‘0) = 𝑃)) | 
| 39 | 38 | simp2d 1143 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄)) | 
| 40 |  | cvmlift3lem6.i | . . . . . . . . . . 11
⊢ 𝐼 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑁) ∧ (𝑔‘0) = (𝐻‘𝑋))) | 
| 41 |  | cnco 23275 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽)) | 
| 42 | 8, 24, 41 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽)) | 
| 43 |  | cvmlift3.l | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
PConn) | 
| 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 35327 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:𝑌⟶𝐵) | 
| 47 |  | cvmlift3lem7.3 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ⊆ (◡𝐺 “ 𝐴)) | 
| 48 |  | cnvimass 6099 | . . . . . . . . . . . . . . 15
⊢ (◡𝐺 “ 𝐴) ⊆ dom 𝐺 | 
| 49 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 50 | 30, 49 | cnf 23255 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) | 
| 51 | 24, 50 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽) | 
| 52 | 48, 51 | fssdm 6754 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐺 “ 𝐴) ⊆ 𝑌) | 
| 53 | 47, 52 | sstrd 3993 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ⊆ 𝑌) | 
| 54 |  | cvmlift3lem6.x | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝑀) | 
| 55 | 53, 54 | sseldd 3983 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑌) | 
| 56 | 46, 55 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝐵) | 
| 57 | 12 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝑁‘0)) = (𝐺‘𝑋)) | 
| 58 | 29, 30 | cnf 23255 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (II Cn 𝐾) → 𝑁:(0[,]1)⟶𝑌) | 
| 59 | 8, 58 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑌) | 
| 60 |  | fvco3 7007 | . . . . . . . . . . . . 13
⊢ ((𝑁:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) →
((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0))) | 
| 61 | 59, 33, 60 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0))) | 
| 62 |  | fvco3 7007 | . . . . . . . . . . . . . 14
⊢ ((𝐻:𝑌⟶𝐵 ∧ 𝑋 ∈ 𝑌) → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) | 
| 63 | 46, 55, 62 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) | 
| 64 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem5 35329 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) | 
| 65 | 64 | fveq1d 6907 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐺‘𝑋)) | 
| 66 | 63, 65 | eqtr3d 2778 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = (𝐺‘𝑋)) | 
| 67 | 57, 61, 66 | 3eqtr4rd 2787 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = ((𝐺 ∘ 𝑁)‘0)) | 
| 68 | 21, 40, 23, 42, 56, 67 | cvmliftiota 35307 | . . . . . . . . . 10
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁) ∧ (𝐼‘0) = (𝐻‘𝑋))) | 
| 69 | 68 | simp2d 1143 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁)) | 
| 70 | 39, 69 | oveq12d 7450 | . . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘ 𝑅)(*𝑝‘𝐽)(𝐹 ∘ 𝐼)) = ((𝐺 ∘ 𝑄)(*𝑝‘𝐽)(𝐺 ∘ 𝑁))) | 
| 71 | 38 | simp1d 1142 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (II Cn 𝐶)) | 
| 72 | 68 | simp1d 1142 | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐶)) | 
| 73 | 9 | simp3d 1144 | . . . . . . . . . 10
⊢ (𝜑 → (𝑅‘1) = (𝐻‘𝑋)) | 
| 74 | 68 | simp3d 1144 | . . . . . . . . . 10
⊢ (𝜑 → (𝐼‘0) = (𝐻‘𝑋)) | 
| 75 | 73, 74 | eqtr4d 2779 | . . . . . . . . 9
⊢ (𝜑 → (𝑅‘1) = (𝐼‘0)) | 
| 76 |  | cvmcn 35268 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) | 
| 77 | 23, 76 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽)) | 
| 78 | 71, 72, 75, 77 | copco 25052 | . . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = ((𝐹 ∘ 𝑅)(*𝑝‘𝐽)(𝐹 ∘ 𝐼))) | 
| 79 | 1, 8, 13, 24 | copco 25052 | . . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) = ((𝐺 ∘ 𝑄)(*𝑝‘𝐽)(𝐺 ∘ 𝑁))) | 
| 80 | 70, 78, 79 | 3eqtr4d 2786 | . . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))) | 
| 81 | 71, 72 | pco0 25048 | . . . . . . . 8
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘0) = (𝑅‘0)) | 
| 82 | 38 | simp3d 1144 | . . . . . . . 8
⊢ (𝜑 → (𝑅‘0) = 𝑃) | 
| 83 | 81, 82 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) | 
| 84 | 71, 72, 75 | pcocn 25051 | . . . . . . . 8
⊢ (𝜑 → (𝑅(*𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶)) | 
| 85 |  | cnco 23275 | . . . . . . . . . 10
⊢ (((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) | 
| 86 | 14, 24, 85 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) | 
| 87 | 17 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0)) = (𝐺‘𝑂)) | 
| 88 | 29, 30 | cnf 23255 | . . . . . . . . . . . 12
⊢ ((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) → (𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌) | 
| 89 | 14, 88 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌) | 
| 90 |  | fvco3 7007 | . . . . . . . . . . 11
⊢ (((𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0))) | 
| 91 | 89, 33, 90 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0))) | 
| 92 | 87, 91, 36 | 3eqtr4rd 2787 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0)) | 
| 93 | 21 | cvmlift 35305 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) | 
| 94 | 23, 86, 27, 92, 93 | syl22anc 838 | . . . . . . . 8
⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) | 
| 95 |  | coeq2 5868 | . . . . . . . . . . 11
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼))) | 
| 96 | 95 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ↔ (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)))) | 
| 97 |  | fveq1 6904 | . . . . . . . . . . 11
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (𝑔‘0) = ((𝑅(*𝑝‘𝐶)𝐼)‘0)) | 
| 98 | 97 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → ((𝑔‘0) = 𝑃 ↔ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃)) | 
| 99 | 96, 98 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃))) | 
| 100 | 99 | riota2 7414 | . . . . . . . 8
⊢ (((𝑅(*𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼))) | 
| 101 | 84, 94, 100 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼))) | 
| 102 | 80, 83, 101 | mpbi2and 712 | . . . . . 6
⊢ (𝜑 → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼)) | 
| 103 | 102 | fveq1d 6907 | . . . . 5
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = ((𝑅(*𝑝‘𝐶)𝐼)‘1)) | 
| 104 | 71, 72 | pco1 25049 | . . . . 5
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘1) = (𝐼‘1)) | 
| 105 | 103, 104 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) | 
| 106 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝑓‘0) = ((𝑄(*𝑝‘𝐾)𝑁)‘0)) | 
| 107 | 106 | eqeq1d 2738 | . . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝑓‘0) = 𝑂 ↔ ((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂)) | 
| 108 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝑓‘1) = ((𝑄(*𝑝‘𝐾)𝑁)‘1)) | 
| 109 | 108 | eqeq1d 2738 | . . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝑓‘1) = 𝑍 ↔ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍)) | 
| 110 |  | coeq2 5868 | . . . . . . . . . . 11
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝐺 ∘ 𝑓) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))) | 
| 111 | 110 | eqeq2d 2747 | . . . . . . . . . 10
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)))) | 
| 112 | 111 | anbi1d 631 | . . . . . . . . 9
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))) | 
| 113 | 112 | riotabidv 7391 | . . . . . . . 8
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))) | 
| 114 | 113 | fveq1d 6907 | . . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1)) | 
| 115 | 114 | eqeq1d 2738 | . . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1) ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) | 
| 116 | 107, 109,
115 | 3anbi123d 1437 | . . . . 5
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) ↔ (((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) | 
| 117 | 116 | rspcev 3621 | . . . 4
⊢ (((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ (((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) | 
| 118 | 14, 17, 20, 105, 117 | syl13anc 1373 | . . 3
⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) | 
| 119 |  | cvmlift3lem6.z | . . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑀) | 
| 120 | 53, 119 | sseldd 3983 | . . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑌) | 
| 121 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem4 35328 | . . . 4
⊢ ((𝜑 ∧ 𝑍 ∈ 𝑌) → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) | 
| 122 | 120, 121 | mpdan 687 | . . 3
⊢ (𝜑 → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) | 
| 123 | 118, 122 | mpbird 257 | . 2
⊢ (𝜑 → (𝐻‘𝑍) = (𝐼‘1)) | 
| 124 |  | iiconn 24914 | . . . . 5
⊢ II ∈
Conn | 
| 125 | 124 | a1i 11 | . . . 4
⊢ (𝜑 → II ∈
Conn) | 
| 126 |  | cvmtop1 35266 | . . . . . . . 8
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) | 
| 127 | 23, 126 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Top) | 
| 128 | 21 | toptopon 22924 | . . . . . . 7
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) | 
| 129 | 127, 128 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) | 
| 130 | 69 | rneqd 5948 | . . . . . . . . 9
⊢ (𝜑 → ran (𝐹 ∘ 𝐼) = ran (𝐺 ∘ 𝑁)) | 
| 131 |  | rnco2 6272 | . . . . . . . . 9
⊢ ran
(𝐹 ∘ 𝐼) = (𝐹 “ ran 𝐼) | 
| 132 |  | rnco2 6272 | . . . . . . . . 9
⊢ ran
(𝐺 ∘ 𝑁) = (𝐺 “ ran 𝑁) | 
| 133 | 130, 131,
132 | 3eqtr3g 2799 | . . . . . . . 8
⊢ (𝜑 → (𝐹 “ ran 𝐼) = (𝐺 “ ran 𝑁)) | 
| 134 |  | iitopon 24906 | . . . . . . . . . . . . 13
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 135 | 134 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) | 
| 136 | 30 | toptopon 22924 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) | 
| 137 | 4, 136 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | 
| 138 |  | resttopon 23170 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑀 ⊆ 𝑌) → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) | 
| 139 | 137, 53, 138 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) | 
| 140 |  | cnf2 23258 | . . . . . . . . . . . 12
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀) ∧ 𝑁 ∈ (II Cn (𝐾 ↾t 𝑀))) → 𝑁:(0[,]1)⟶𝑀) | 
| 141 | 135, 139,
7, 140 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑀) | 
| 142 | 141 | frnd 6743 | . . . . . . . . . 10
⊢ (𝜑 → ran 𝑁 ⊆ 𝑀) | 
| 143 | 142, 47 | sstrd 3993 | . . . . . . . . 9
⊢ (𝜑 → ran 𝑁 ⊆ (◡𝐺 “ 𝐴)) | 
| 144 | 51 | ffund 6739 | . . . . . . . . . 10
⊢ (𝜑 → Fun 𝐺) | 
| 145 | 143, 48 | sstrdi 3995 | . . . . . . . . . 10
⊢ (𝜑 → ran 𝑁 ⊆ dom 𝐺) | 
| 146 |  | funimass3 7073 | . . . . . . . . . 10
⊢ ((Fun
𝐺 ∧ ran 𝑁 ⊆ dom 𝐺) → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (◡𝐺 “ 𝐴))) | 
| 147 | 144, 145,
146 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (◡𝐺 “ 𝐴))) | 
| 148 | 143, 147 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → (𝐺 “ ran 𝑁) ⊆ 𝐴) | 
| 149 | 133, 148 | eqsstrd 4017 | . . . . . . 7
⊢ (𝜑 → (𝐹 “ ran 𝐼) ⊆ 𝐴) | 
| 150 | 21, 49 | cnf 23255 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) | 
| 151 | 77, 150 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽) | 
| 152 | 151 | ffund 6739 | . . . . . . . 8
⊢ (𝜑 → Fun 𝐹) | 
| 153 | 29, 21 | cnf 23255 | . . . . . . . . . . 11
⊢ (𝐼 ∈ (II Cn 𝐶) → 𝐼:(0[,]1)⟶𝐵) | 
| 154 | 72, 153 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐼:(0[,]1)⟶𝐵) | 
| 155 | 154 | frnd 6743 | . . . . . . . . 9
⊢ (𝜑 → ran 𝐼 ⊆ 𝐵) | 
| 156 | 151 | fdmd 6745 | . . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐵) | 
| 157 | 155, 156 | sseqtrrd 4020 | . . . . . . . 8
⊢ (𝜑 → ran 𝐼 ⊆ dom 𝐹) | 
| 158 |  | funimass3 7073 | . . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐼 ⊆ dom 𝐹) → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (◡𝐹 “ 𝐴))) | 
| 159 | 152, 157,
158 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (◡𝐹 “ 𝐴))) | 
| 160 | 149, 159 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ran 𝐼 ⊆ (◡𝐹 “ 𝐴)) | 
| 161 |  | cnvimass 6099 | . . . . . . 7
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 | 
| 162 | 161, 151 | fssdm 6754 | . . . . . 6
⊢ (𝜑 → (◡𝐹 “ 𝐴) ⊆ 𝐵) | 
| 163 |  | cnrest2 23295 | . . . . . 6
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran 𝐼 ⊆ (◡𝐹 “ 𝐴) ∧ (◡𝐹 “ 𝐴) ⊆ 𝐵) → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴))))) | 
| 164 | 129, 160,
162, 163 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴))))) | 
| 165 | 72, 164 | mpbid 232 | . . . 4
⊢ (𝜑 → 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴)))) | 
| 166 |  | cvmlift3lem7.2 | . . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) | 
| 167 |  | cvmlift3lem7.s | . . . . . . . 8
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) | 
| 168 | 167 | cvmsss 35273 | . . . . . . 7
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝑇 ⊆ 𝐶) | 
| 169 | 166, 168 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑇 ⊆ 𝐶) | 
| 170 |  | cvmlift3lem7.1 | . . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴) | 
| 171 | 66, 170 | eqeltrd 2840 | . . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) ∈ 𝐴) | 
| 172 |  | cvmlift3lem7.w | . . . . . . . . 9
⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏) | 
| 173 | 167, 21, 172 | cvmsiota 35283 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝐴) ∧ (𝐻‘𝑋) ∈ 𝐵 ∧ (𝐹‘(𝐻‘𝑋)) ∈ 𝐴)) → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) | 
| 174 | 23, 166, 56, 171, 173 | syl13anc 1373 | . . . . . . 7
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) | 
| 175 | 174 | simpld 494 | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝑇) | 
| 176 | 169, 175 | sseldd 3983 | . . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝐶) | 
| 177 |  | elssuni 4936 | . . . . . . 7
⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇) | 
| 178 | 175, 177 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇) | 
| 179 | 167 | cvmsuni 35275 | . . . . . . 7
⊢ (𝑇 ∈ (𝑆‘𝐴) → ∪ 𝑇 = (◡𝐹 “ 𝐴)) | 
| 180 | 166, 179 | syl 17 | . . . . . 6
⊢ (𝜑 → ∪ 𝑇 =
(◡𝐹 “ 𝐴)) | 
| 181 | 178, 180 | sseqtrd 4019 | . . . . 5
⊢ (𝜑 → 𝑊 ⊆ (◡𝐹 “ 𝐴)) | 
| 182 | 167 | cvmsrcl 35270 | . . . . . . . 8
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝐴 ∈ 𝐽) | 
| 183 | 166, 182 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝐽) | 
| 184 |  | cnima 23274 | . . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ 𝐶) | 
| 185 | 77, 183, 184 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (◡𝐹 “ 𝐴) ∈ 𝐶) | 
| 186 |  | restopn2 23186 | . . . . . 6
⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝐴) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝐴)))) | 
| 187 | 127, 185,
186 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝐴)))) | 
| 188 | 176, 181,
187 | mpbir2and 713 | . . . 4
⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴))) | 
| 189 | 167 | cvmscld 35279 | . . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝐴) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝐴)))) | 
| 190 | 23, 166, 175, 189 | syl3anc 1372 | . . . 4
⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝐴)))) | 
| 191 | 33 | a1i 11 | . . . 4
⊢ (𝜑 → 0 ∈
(0[,]1)) | 
| 192 | 174 | simprd 495 | . . . . 5
⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝑊) | 
| 193 | 74, 192 | eqeltrd 2840 | . . . 4
⊢ (𝜑 → (𝐼‘0) ∈ 𝑊) | 
| 194 | 29, 125, 165, 188, 190, 191, 193 | conncn 23435 | . . 3
⊢ (𝜑 → 𝐼:(0[,]1)⟶𝑊) | 
| 195 |  | 1elunit 13511 | . . 3
⊢ 1 ∈
(0[,]1) | 
| 196 |  | ffvelcdm 7100 | . . 3
⊢ ((𝐼:(0[,]1)⟶𝑊 ∧ 1 ∈ (0[,]1)) →
(𝐼‘1) ∈ 𝑊) | 
| 197 | 194, 195,
196 | sylancl 586 | . 2
⊢ (𝜑 → (𝐼‘1) ∈ 𝑊) | 
| 198 | 123, 197 | eqeltrd 2840 | 1
⊢ (𝜑 → (𝐻‘𝑍) ∈ 𝑊) |