| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ (𝐻‘𝑦) = (𝐻‘𝑦) |
| 2 | | cvmlift3.b |
. . . . . 6
⊢ 𝐵 = ∪
𝐶 |
| 3 | | cvmlift3.y |
. . . . . 6
⊢ 𝑌 = ∪
𝐾 |
| 4 | | cvmlift3.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 5 | | cvmlift3.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ SConn) |
| 6 | | cvmlift3.l |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
PConn) |
| 7 | | cvmlift3.o |
. . . . . 6
⊢ (𝜑 → 𝑂 ∈ 𝑌) |
| 8 | | cvmlift3.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) |
| 9 | | cvmlift3.p |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
| 10 | | cvmlift3.e |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) |
| 11 | | cvmlift3.h |
. . . . . 6
⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) |
| 12 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem4 35327 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ((𝐻‘𝑦) = (𝐻‘𝑦) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦)))) |
| 13 | 1, 12 | mpbii 233 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦))) |
| 14 | | df-3an 1089 |
. . . . . 6
⊢ (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦)) ↔ (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦) ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦))) |
| 15 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(℩𝑔
∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) |
| 16 | 4 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 17 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → 𝑓 ∈ (II Cn 𝐾)) |
| 18 | 8 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → 𝐺 ∈ (𝐾 Cn 𝐽)) |
| 19 | | cnco 23274 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑓) ∈ (II Cn 𝐽)) |
| 20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝐺 ∘ 𝑓) ∈ (II Cn 𝐽)) |
| 21 | 9 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → 𝑃 ∈ 𝐵) |
| 22 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝑓‘0) = 𝑂) |
| 23 | 22 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝐺‘(𝑓‘0)) = (𝐺‘𝑂)) |
| 24 | | iiuni 24907 |
. . . . . . . . . . . . . . . 16
⊢ (0[,]1) =
∪ II |
| 25 | 24, 3 | cnf 23254 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (II Cn 𝐾) → 𝑓:(0[,]1)⟶𝑌) |
| 26 | 17, 25 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → 𝑓:(0[,]1)⟶𝑌) |
| 27 | | 0elunit 13509 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
(0[,]1) |
| 28 | | fvco3 7008 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) →
((𝐺 ∘ 𝑓)‘0) = (𝐺‘(𝑓‘0))) |
| 29 | 26, 27, 28 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → ((𝐺 ∘ 𝑓)‘0) = (𝐺‘(𝑓‘0))) |
| 30 | 10 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝐹‘𝑃) = (𝐺‘𝑂)) |
| 31 | 23, 29, 30 | 3eqtr4rd 2788 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝐹‘𝑃) = ((𝐺 ∘ 𝑓)‘0)) |
| 32 | 2, 15, 16, 20, 21, 31 | cvmliftiota 35306 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) ∈ (II Cn 𝐶) ∧ (𝐹 ∘ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))) = (𝐺 ∘ 𝑓) ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘0) = 𝑃)) |
| 33 | 32 | simp2d 1144 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝐹 ∘ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))) = (𝐺 ∘ 𝑓)) |
| 34 | 33 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → ((𝐹 ∘ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)))‘1) = ((𝐺 ∘ 𝑓)‘1)) |
| 35 | 32 | simp1d 1143 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) ∈ (II Cn 𝐶)) |
| 36 | 24, 2 | cnf 23254 |
. . . . . . . . . . 11
⊢
((℩𝑔
∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) ∈ (II Cn 𝐶) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)):(0[,]1)⟶𝐵) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)):(0[,]1)⟶𝐵) |
| 38 | | 1elunit 13510 |
. . . . . . . . . 10
⊢ 1 ∈
(0[,]1) |
| 39 | | fvco3 7008 |
. . . . . . . . . 10
⊢
(((℩𝑔
∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)):(0[,]1)⟶𝐵 ∧ 1 ∈ (0[,]1)) → ((𝐹 ∘ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)))‘1) = (𝐹‘((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1))) |
| 40 | 37, 38, 39 | sylancl 586 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → ((𝐹 ∘ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)))‘1) = (𝐹‘((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1))) |
| 41 | | fvco3 7008 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶𝑌 ∧ 1 ∈ (0[,]1)) →
((𝐺 ∘ 𝑓)‘1) = (𝐺‘(𝑓‘1))) |
| 42 | 26, 38, 41 | sylancl 586 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → ((𝐺 ∘ 𝑓)‘1) = (𝐺‘(𝑓‘1))) |
| 43 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝑓‘1) = 𝑦) |
| 44 | 43 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝐺‘(𝑓‘1)) = (𝐺‘𝑦)) |
| 45 | 42, 44 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → ((𝐺 ∘ 𝑓)‘1) = (𝐺‘𝑦)) |
| 46 | 34, 40, 45 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (𝐹‘((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1)) = (𝐺‘𝑦)) |
| 47 | | fveqeq2 6915 |
. . . . . . . 8
⊢
(((℩𝑔
∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦) → ((𝐹‘((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1)) = (𝐺‘𝑦) ↔ (𝐹‘(𝐻‘𝑦)) = (𝐺‘𝑦))) |
| 48 | 46, 47 | syl5ibcom 245 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) ∧ ((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦)) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦) → (𝐹‘(𝐻‘𝑦)) = (𝐺‘𝑦))) |
| 49 | 48 | expimpd 453 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) → ((((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦) ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦)) → (𝐹‘(𝐻‘𝑦)) = (𝐺‘𝑦))) |
| 50 | 14, 49 | biimtrid 242 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑓 ∈ (II Cn 𝐾)) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦)) → (𝐹‘(𝐻‘𝑦)) = (𝐺‘𝑦))) |
| 51 | 50 | rexlimdva 3155 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑦 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐻‘𝑦)) → (𝐹‘(𝐻‘𝑦)) = (𝐺‘𝑦))) |
| 52 | 13, 51 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐹‘(𝐻‘𝑦)) = (𝐺‘𝑦)) |
| 53 | 52 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ (𝐹‘(𝐻‘𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝐺‘𝑦))) |
| 54 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem3 35326 |
. . . 4
⊢ (𝜑 → 𝐻:𝑌⟶𝐵) |
| 55 | 54 | ffvelcdmda 7104 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐻‘𝑦) ∈ 𝐵) |
| 56 | 54 | feqmptd 6977 |
. . 3
⊢ (𝜑 → 𝐻 = (𝑦 ∈ 𝑌 ↦ (𝐻‘𝑦))) |
| 57 | | cvmcn 35267 |
. . . . 5
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
| 58 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 59 | 2, 58 | cnf 23254 |
. . . . 5
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
| 60 | 4, 57, 59 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽) |
| 61 | 60 | feqmptd 6977 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑤 ∈ 𝐵 ↦ (𝐹‘𝑤))) |
| 62 | | fveq2 6906 |
. . 3
⊢ (𝑤 = (𝐻‘𝑦) → (𝐹‘𝑤) = (𝐹‘(𝐻‘𝑦))) |
| 63 | 55, 56, 61, 62 | fmptco 7149 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐻) = (𝑦 ∈ 𝑌 ↦ (𝐹‘(𝐻‘𝑦)))) |
| 64 | 3, 58 | cnf 23254 |
. . . 4
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) |
| 65 | 8, 64 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽) |
| 66 | 65 | feqmptd 6977 |
. 2
⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝑌 ↦ (𝐺‘𝑦))) |
| 67 | 53, 63, 66 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) |