| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cvmlift3.b | . . . 4
⊢ 𝐵 = ∪
𝐶 | 
| 2 |  | cvmlift3.y | . . . 4
⊢ 𝑌 = ∪
𝐾 | 
| 3 |  | cvmlift3lem7.s | . . . 4
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) | 
| 4 |  | cvmlift3.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) | 
| 5 |  | cvmlift3.k | . . . . 5
⊢ (𝜑 → 𝐾 ∈ SConn) | 
| 6 |  | cvmlift3.l | . . . . 5
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
PConn) | 
| 7 |  | cvmlift3.o | . . . . 5
⊢ (𝜑 → 𝑂 ∈ 𝑌) | 
| 8 |  | cvmlift3.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) | 
| 9 |  | cvmlift3.p | . . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐵) | 
| 10 |  | cvmlift3.e | . . . . 5
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) | 
| 11 |  | cvmlift3.h | . . . . 5
⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) | 
| 12 | 1, 2, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem3 35326 | . . . 4
⊢ (𝜑 → 𝐻:𝑌⟶𝐵) | 
| 13 | 1, 2, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem5 35328 | . . . . 5
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) | 
| 14 | 13, 8 | eqeltrd 2841 | . . . 4
⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽)) | 
| 15 |  | sconntop 35233 | . . . . 5
⊢ (𝐾 ∈ SConn → 𝐾 ∈ Top) | 
| 16 | 5, 15 | syl 17 | . . . 4
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 17 |  | cvmlift3lem7.3 | . . . . . 6
⊢ (𝜑 → 𝑀 ⊆ (◡𝐺 “ 𝐴)) | 
| 18 |  | cnvimass 6100 | . . . . . . 7
⊢ (◡𝐺 “ 𝐴) ⊆ dom 𝐺 | 
| 19 |  | eqid 2737 | . . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 20 | 2, 19 | cnf 23254 | . . . . . . . 8
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) | 
| 21 |  | fdm 6745 | . . . . . . . 8
⊢ (𝐺:𝑌⟶∪ 𝐽 → dom 𝐺 = 𝑌) | 
| 22 | 8, 20, 21 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → dom 𝐺 = 𝑌) | 
| 23 | 18, 22 | sseqtrid 4026 | . . . . . 6
⊢ (𝜑 → (◡𝐺 “ 𝐴) ⊆ 𝑌) | 
| 24 | 17, 23 | sstrd 3994 | . . . . 5
⊢ (𝜑 → 𝑀 ⊆ 𝑌) | 
| 25 |  | cvmlift3lem7.5 | . . . . . 6
⊢ (𝜑 → 𝑉 ⊆ 𝑀) | 
| 26 |  | cvmlift3lem7.6 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 27 | 25, 26 | sseldd 3984 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑀) | 
| 28 | 24, 27 | sseldd 3984 | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑌) | 
| 29 |  | cvmlift3lem7.2 | . . . 4
⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) | 
| 30 | 12, 28 | ffvelcdmd 7105 | . . . . 5
⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝐵) | 
| 31 |  | fvco3 7008 | . . . . . . . 8
⊢ ((𝐻:𝑌⟶𝐵 ∧ 𝑋 ∈ 𝑌) → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) | 
| 32 | 12, 28, 31 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) | 
| 33 | 13 | fveq1d 6908 | . . . . . . 7
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐺‘𝑋)) | 
| 34 | 32, 33 | eqtr3d 2779 | . . . . . 6
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = (𝐺‘𝑋)) | 
| 35 |  | cvmlift3lem7.1 | . . . . . 6
⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴) | 
| 36 | 34, 35 | eqeltrd 2841 | . . . . 5
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) ∈ 𝐴) | 
| 37 |  | cvmlift3lem7.w | . . . . . 6
⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏) | 
| 38 | 3, 1, 37 | cvmsiota 35282 | . . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝐴) ∧ (𝐻‘𝑋) ∈ 𝐵 ∧ (𝐹‘(𝐻‘𝑋)) ∈ 𝐴)) → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) | 
| 39 | 4, 29, 30, 36, 38 | syl13anc 1374 | . . . 4
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) | 
| 40 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝐻‘𝑋) = (𝐻‘𝑋) | 
| 41 | 1, 2, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem4 35327 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ((𝐻‘𝑋) = (𝐻‘𝑋) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑋)))) | 
| 42 | 40, 41 | mpbii 233 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑋))) | 
| 43 | 28, 42 | mpdan 687 | . . . . . . . . 9
⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑋))) | 
| 44 | 43 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑋))) | 
| 45 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑓 = ℎ → (𝑓‘0) = (ℎ‘0)) | 
| 46 | 45 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (𝑓 = ℎ → ((𝑓‘0) = 𝑂 ↔ (ℎ‘0) = 𝑂)) | 
| 47 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑓 = ℎ → (𝑓‘1) = (ℎ‘1)) | 
| 48 | 47 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (𝑓 = ℎ → ((𝑓‘1) = 𝑋 ↔ (ℎ‘1) = 𝑋)) | 
| 49 |  | coeq2 5869 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 = ℎ → (𝐺 ∘ 𝑓) = (𝐺 ∘ ℎ)) | 
| 50 | 49 | eqeq2d 2748 | . . . . . . . . . . . . . . 15
⊢ (𝑓 = ℎ → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ ℎ))) | 
| 51 | 50 | anbi1d 631 | . . . . . . . . . . . . . 14
⊢ (𝑓 = ℎ → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ ℎ) ∧ (𝑔‘0) = 𝑃))) | 
| 52 | 51 | riotabidv 7390 | . . . . . . . . . . . . 13
⊢ (𝑓 = ℎ → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ℎ) ∧ (𝑔‘0) = 𝑃))) | 
| 53 |  | coeq2 5869 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑔 → (𝐹 ∘ 𝑎) = (𝐹 ∘ 𝑔)) | 
| 54 | 53 | eqeq1d 2739 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑔 → ((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ ℎ))) | 
| 55 |  | fveq1 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑔 → (𝑎‘0) = (𝑔‘0)) | 
| 56 | 55 | eqeq1d 2739 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑔 → ((𝑎‘0) = 𝑃 ↔ (𝑔‘0) = 𝑃)) | 
| 57 | 54, 56 | anbi12d 632 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑔 → (((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ ℎ) ∧ (𝑔‘0) = 𝑃))) | 
| 58 | 57 | cbvriotavw 7398 | . . . . . . . . . . . . 13
⊢
(℩𝑎
∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ℎ) ∧ (𝑔‘0) = 𝑃)) | 
| 59 | 52, 58 | eqtr4di 2795 | . . . . . . . . . . . 12
⊢ (𝑓 = ℎ → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))) | 
| 60 | 59 | fveq1d 6908 | . . . . . . . . . . 11
⊢ (𝑓 = ℎ → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1)) | 
| 61 | 60 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (𝑓 = ℎ → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑋) ↔ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋))) | 
| 62 | 46, 48, 61 | 3anbi123d 1438 | . . . . . . . . 9
⊢ (𝑓 = ℎ → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ↔ ((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)))) | 
| 63 | 62 | cbvrexvw 3238 | . . . . . . . 8
⊢
(∃𝑓 ∈ (II
Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ↔ ∃ℎ ∈ (II Cn 𝐾)((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋))) | 
| 64 | 44, 63 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∃ℎ ∈ (II Cn 𝐾)((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋))) | 
| 65 |  | cvmlift3lem7.7 | . . . . . . . . 9
⊢ (𝜑 → (𝐾 ↾t 𝑀) ∈ PConn) | 
| 66 | 65 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝐾 ↾t 𝑀) ∈ PConn) | 
| 67 | 2 | restuni 23170 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ Top ∧ 𝑀 ⊆ 𝑌) → 𝑀 = ∪ (𝐾 ↾t 𝑀)) | 
| 68 | 16, 24, 67 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 = ∪ (𝐾 ↾t 𝑀)) | 
| 69 | 27, 68 | eleqtrd 2843 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ∪ (𝐾 ↾t 𝑀)) | 
| 70 | 69 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑋 ∈ ∪ (𝐾 ↾t 𝑀)) | 
| 71 | 68 | eleq2d 2827 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ 𝑀 ↔ 𝑦 ∈ ∪ (𝐾 ↾t 𝑀))) | 
| 72 | 71 | biimpa 476 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ∪ (𝐾 ↾t 𝑀)) | 
| 73 |  | eqid 2737 | . . . . . . . . 9
⊢ ∪ (𝐾
↾t 𝑀) =
∪ (𝐾 ↾t 𝑀) | 
| 74 | 73 | pconncn 35229 | . . . . . . . 8
⊢ (((𝐾 ↾t 𝑀) ∈ PConn ∧ 𝑋 ∈ ∪ (𝐾
↾t 𝑀)
∧ 𝑦 ∈ ∪ (𝐾
↾t 𝑀))
→ ∃𝑛 ∈ (II
Cn (𝐾 ↾t
𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) | 
| 75 | 66, 70, 72, 74 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∃𝑛 ∈ (II Cn (𝐾 ↾t 𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) | 
| 76 |  | reeanv 3229 | . . . . . . . 8
⊢
(∃ℎ ∈ (II
Cn 𝐾)∃𝑛 ∈ (II Cn (𝐾 ↾t 𝑀))(((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) ↔ (∃ℎ ∈ (II Cn 𝐾)((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ∃𝑛 ∈ (II Cn (𝐾 ↾t 𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) | 
| 77 | 4 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐹 ∈ (𝐶 CovMap 𝐽)) | 
| 78 | 5 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐾 ∈ SConn) | 
| 79 | 6 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐾 ∈ 𝑛-Locally
PConn) | 
| 80 | 7 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑂 ∈ 𝑌) | 
| 81 | 8 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝐺 ∈ (𝐾 Cn 𝐽)) | 
| 82 | 9 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑃 ∈ 𝐵) | 
| 83 | 10 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → (𝐹‘𝑃) = (𝐺‘𝑂)) | 
| 84 | 35 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → (𝐺‘𝑋) ∈ 𝐴) | 
| 85 | 29 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑇 ∈ (𝑆‘𝐴)) | 
| 86 | 17 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑀 ⊆ (◡𝐺 “ 𝐴)) | 
| 87 | 27 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑋 ∈ 𝑀) | 
| 88 |  | simpllr 776 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑦 ∈ 𝑀) | 
| 89 |  | simplrl 777 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → ℎ ∈ (II Cn 𝐾)) | 
| 90 |  | simprl 771 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → ((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋))) | 
| 91 |  | simplrr 778 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀))) | 
| 92 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) | 
| 93 | 53 | eqeq1d 2739 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑔 → ((𝐹 ∘ 𝑎) = (𝐺 ∘ 𝑛) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑛))) | 
| 94 | 55 | eqeq1d 2739 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑔 → ((𝑎‘0) = (𝐻‘𝑋) ↔ (𝑔‘0) = (𝐻‘𝑋))) | 
| 95 | 93, 94 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑔 → (((𝐹 ∘ 𝑎) = (𝐺 ∘ 𝑛) ∧ (𝑎‘0) = (𝐻‘𝑋)) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑛) ∧ (𝑔‘0) = (𝐻‘𝑋)))) | 
| 96 | 95 | cbvriotavw 7398 | . . . . . . . . . . 11
⊢
(℩𝑎
∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ 𝑛) ∧ (𝑎‘0) = (𝐻‘𝑋))) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑛) ∧ (𝑔‘0) = (𝐻‘𝑋))) | 
| 97 | 1, 2, 77, 78, 79, 80, 81, 82, 83, 11, 3, 84, 85, 86, 37, 87, 88, 89, 58, 90, 91, 92, 96 | cvmlift3lem6 35329 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) ∧ (((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦))) → (𝐻‘𝑦) ∈ 𝑊) | 
| 98 | 97 | ex 412 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ (ℎ ∈ (II Cn 𝐾) ∧ 𝑛 ∈ (II Cn (𝐾 ↾t 𝑀)))) → ((((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) → (𝐻‘𝑦) ∈ 𝑊)) | 
| 99 | 98 | rexlimdvva 3213 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∃ℎ ∈ (II Cn 𝐾)∃𝑛 ∈ (II Cn (𝐾 ↾t 𝑀))(((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) → (𝐻‘𝑦) ∈ 𝑊)) | 
| 100 | 76, 99 | biimtrrid 243 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((∃ℎ ∈ (II Cn 𝐾)((ℎ‘0) = 𝑂 ∧ (ℎ‘1) = 𝑋 ∧ ((℩𝑎 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑎) = (𝐺 ∘ ℎ) ∧ (𝑎‘0) = 𝑃))‘1) = (𝐻‘𝑋)) ∧ ∃𝑛 ∈ (II Cn (𝐾 ↾t 𝑀))((𝑛‘0) = 𝑋 ∧ (𝑛‘1) = 𝑦)) → (𝐻‘𝑦) ∈ 𝑊)) | 
| 101 | 64, 75, 100 | mp2and 699 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝐻‘𝑦) ∈ 𝑊) | 
| 102 | 101 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝑀 (𝐻‘𝑦) ∈ 𝑊) | 
| 103 | 12 | ffund 6740 | . . . . . 6
⊢ (𝜑 → Fun 𝐻) | 
| 104 | 12 | fdmd 6746 | . . . . . . 7
⊢ (𝜑 → dom 𝐻 = 𝑌) | 
| 105 | 24, 104 | sseqtrrd 4021 | . . . . . 6
⊢ (𝜑 → 𝑀 ⊆ dom 𝐻) | 
| 106 |  | funimass4 6973 | . . . . . 6
⊢ ((Fun
𝐻 ∧ 𝑀 ⊆ dom 𝐻) → ((𝐻 “ 𝑀) ⊆ 𝑊 ↔ ∀𝑦 ∈ 𝑀 (𝐻‘𝑦) ∈ 𝑊)) | 
| 107 | 103, 105,
106 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((𝐻 “ 𝑀) ⊆ 𝑊 ↔ ∀𝑦 ∈ 𝑀 (𝐻‘𝑦) ∈ 𝑊)) | 
| 108 | 102, 107 | mpbird 257 | . . . 4
⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊) | 
| 109 | 1, 2, 3, 4, 12, 14, 16, 28, 29, 39, 24, 108 | cvmlift2lem9a 35308 | . . 3
⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶)) | 
| 110 | 73 | cncnpi 23286 | . . 3
⊢ (((𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶) ∧ 𝑋 ∈ ∪ (𝐾 ↾t 𝑀)) → (𝐻 ↾ 𝑀) ∈ (((𝐾 ↾t 𝑀) CnP 𝐶)‘𝑋)) | 
| 111 | 109, 69, 110 | syl2anc 584 | . 2
⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ (((𝐾 ↾t 𝑀) CnP 𝐶)‘𝑋)) | 
| 112 |  | cvmlift3lem7.4 | . . . . 5
⊢ (𝜑 → 𝑉 ∈ 𝐾) | 
| 113 | 2 | ssntr 23066 | . . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝑀 ⊆ 𝑌) ∧ (𝑉 ∈ 𝐾 ∧ 𝑉 ⊆ 𝑀)) → 𝑉 ⊆ ((int‘𝐾)‘𝑀)) | 
| 114 | 16, 24, 112, 25, 113 | syl22anc 839 | . . . 4
⊢ (𝜑 → 𝑉 ⊆ ((int‘𝐾)‘𝑀)) | 
| 115 | 114, 26 | sseldd 3984 | . . 3
⊢ (𝜑 → 𝑋 ∈ ((int‘𝐾)‘𝑀)) | 
| 116 | 2, 1 | cnprest 23297 | . . 3
⊢ (((𝐾 ∈ Top ∧ 𝑀 ⊆ 𝑌) ∧ (𝑋 ∈ ((int‘𝐾)‘𝑀) ∧ 𝐻:𝑌⟶𝐵)) → (𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋) ↔ (𝐻 ↾ 𝑀) ∈ (((𝐾 ↾t 𝑀) CnP 𝐶)‘𝑋))) | 
| 117 | 16, 24, 115, 12, 116 | syl22anc 839 | . 2
⊢ (𝜑 → (𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋) ↔ (𝐻 ↾ 𝑀) ∈ (((𝐾 ↾t 𝑀) CnP 𝐶)‘𝑋))) | 
| 118 | 111, 117 | mpbird 257 | 1
⊢ (𝜑 → 𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋)) |