Proof of Theorem cvmlift3lem9
| Step | Hyp | Ref
| Expression |
| 1 | | cvmlift3.b |
. . 3
⊢ 𝐵 = ∪
𝐶 |
| 2 | | cvmlift3.y |
. . 3
⊢ 𝑌 = ∪
𝐾 |
| 3 | | cvmlift3.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 4 | | cvmlift3.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ SConn) |
| 5 | | cvmlift3.l |
. . 3
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
PConn) |
| 6 | | cvmlift3.o |
. . 3
⊢ (𝜑 → 𝑂 ∈ 𝑌) |
| 7 | | cvmlift3.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) |
| 8 | | cvmlift3.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
| 9 | | cvmlift3.e |
. . 3
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) |
| 10 | | cvmlift3.h |
. . 3
⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) |
| 11 | | cvmlift3lem7.s |
. . 3
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
| 12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | cvmlift3lem8 35331 |
. 2
⊢ (𝜑 → 𝐻 ∈ (𝐾 Cn 𝐶)) |
| 13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cvmlift3lem5 35328 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) |
| 14 | | iitopon 24905 |
. . . . . 6
⊢ II ∈
(TopOn‘(0[,]1)) |
| 15 | 14 | a1i 11 |
. . . . 5
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
| 16 | | sconntop 35233 |
. . . . . . 7
⊢ (𝐾 ∈ SConn → 𝐾 ∈ Top) |
| 17 | 4, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
| 18 | 2 | toptopon 22923 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
| 19 | 17, 18 | sylib 218 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
| 20 | | cnconst2 23291 |
. . . . 5
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑂 ∈ 𝑌) → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾)) |
| 21 | 15, 19, 6, 20 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾)) |
| 22 | | 0elunit 13509 |
. . . . 5
⊢ 0 ∈
(0[,]1) |
| 23 | | fvconst2g 7222 |
. . . . 5
⊢ ((𝑂 ∈ 𝑌 ∧ 0 ∈ (0[,]1)) → (((0[,]1)
× {𝑂})‘0) =
𝑂) |
| 24 | 6, 22, 23 | sylancl 586 |
. . . 4
⊢ (𝜑 → (((0[,]1) × {𝑂})‘0) = 𝑂) |
| 25 | | 1elunit 13510 |
. . . . 5
⊢ 1 ∈
(0[,]1) |
| 26 | | fvconst2g 7222 |
. . . . 5
⊢ ((𝑂 ∈ 𝑌 ∧ 1 ∈ (0[,]1)) → (((0[,]1)
× {𝑂})‘1) =
𝑂) |
| 27 | 6, 25, 26 | sylancl 586 |
. . . 4
⊢ (𝜑 → (((0[,]1) × {𝑂})‘1) = 𝑂) |
| 28 | 9 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝜑 → {(𝐹‘𝑃)} = {(𝐺‘𝑂)}) |
| 29 | 28 | xpeq2d 5715 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]1) × {(𝐹‘𝑃)}) = ((0[,]1) × {(𝐺‘𝑂)})) |
| 30 | | cvmcn 35267 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
| 31 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 32 | 1, 31 | cnf 23254 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
| 33 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝐹:𝐵⟶∪ 𝐽 → 𝐹 Fn 𝐵) |
| 34 | 3, 30, 32, 33 | 4syl 19 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐵) |
| 35 | | fcoconst 7154 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐵 ∧ 𝑃 ∈ 𝐵) → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)})) |
| 36 | 34, 8, 35 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)})) |
| 37 | 2, 31 | cnf 23254 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) |
| 38 | 7, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽) |
| 39 | 38 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn 𝑌) |
| 40 | | fcoconst 7154 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝑌 ∧ 𝑂 ∈ 𝑌) → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)})) |
| 41 | 39, 6, 40 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)})) |
| 42 | 29, 36, 41 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂}))) |
| 43 | | fvconst2g 7222 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝐵 ∧ 0 ∈ (0[,]1)) → (((0[,]1)
× {𝑃})‘0) =
𝑃) |
| 44 | 8, 22, 43 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (((0[,]1) × {𝑃})‘0) = 𝑃) |
| 45 | | cvmtop1 35265 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
| 46 | 3, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Top) |
| 47 | 1 | toptopon 22923 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
| 48 | 46, 47 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
| 49 | | cnconst2 23291 |
. . . . . . . . 9
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐶 ∈ (TopOn‘𝐵) ∧ 𝑃 ∈ 𝐵) → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶)) |
| 50 | 15, 48, 8, 49 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶)) |
| 51 | | cvmtop2 35266 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top) |
| 52 | 3, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ Top) |
| 53 | 31 | toptopon 22923 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 54 | 52, 53 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 55 | 38, 6 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑂) ∈ ∪ 𝐽) |
| 56 | | cnconst2 23291 |
. . . . . . . . . . 11
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (𝐺‘𝑂) ∈ ∪ 𝐽)
→ ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽)) |
| 57 | 15, 54, 55, 56 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽)) |
| 58 | 41, 57 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽)) |
| 59 | | fvconst2g 7222 |
. . . . . . . . . . 11
⊢ (((𝐺‘𝑂) ∈ ∪ 𝐽 ∧ 0 ∈ (0[,]1)) →
(((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂)) |
| 60 | 55, 22, 59 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → (((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂)) |
| 61 | 41 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0) = (((0[,]1) × {(𝐺‘𝑂)})‘0)) |
| 62 | 60, 61, 9 | 3eqtr4rd 2788 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0)) |
| 63 | 1 | cvmlift 35304 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) |
| 64 | 3, 58, 8, 62, 63 | syl22anc 839 |
. . . . . . . 8
⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) |
| 65 | | coeq2 5869 |
. . . . . . . . . . 11
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ((0[,]1) × {𝑃}))) |
| 66 | 65 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ↔ (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})))) |
| 67 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝑔‘0) = (((0[,]1) × {𝑃})‘0)) |
| 68 | 67 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝑔‘0) = 𝑃 ↔ (((0[,]1) × {𝑃})‘0) = 𝑃)) |
| 69 | 66, 68 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃))) |
| 70 | 69 | riota2 7413 |
. . . . . . . 8
⊢
((((0[,]1) × {𝑃}) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃}))) |
| 71 | 50, 64, 70 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃}))) |
| 72 | 42, 44, 71 | mpbi2and 712 |
. . . . . 6
⊢ (𝜑 → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃})) |
| 73 | 72 | fveq1d 6908 |
. . . . 5
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = (((0[,]1) × {𝑃})‘1)) |
| 74 | | fvconst2g 7222 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐵 ∧ 1 ∈ (0[,]1)) → (((0[,]1)
× {𝑃})‘1) =
𝑃) |
| 75 | 8, 25, 74 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (((0[,]1) × {𝑃})‘1) = 𝑃) |
| 76 | 73, 75 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃) |
| 77 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘0) = (((0[,]1) × {𝑂})‘0)) |
| 78 | 77 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘0) = 𝑂 ↔ (((0[,]1) × {𝑂})‘0) = 𝑂)) |
| 79 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘1) = (((0[,]1) × {𝑂})‘1)) |
| 80 | 79 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘1) = 𝑂 ↔ (((0[,]1) × {𝑂})‘1) = 𝑂)) |
| 81 | | coeq2 5869 |
. . . . . . . . . . 11
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝐺 ∘ 𝑓) = (𝐺 ∘ ((0[,]1) × {𝑂}))) |
| 82 | 81 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})))) |
| 83 | 82 | anbi1d 631 |
. . . . . . . . 9
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))) |
| 84 | 83 | riotabidv 7390 |
. . . . . . . 8
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))) |
| 85 | 84 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1)) |
| 86 | 85 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃 ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) |
| 87 | 78, 80, 86 | 3anbi123d 1438 |
. . . . 5
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃) ↔ ((((0[,]1) × {𝑂})‘0) = 𝑂 ∧ (((0[,]1) × {𝑂})‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))) |
| 88 | 87 | rspcev 3622 |
. . . 4
⊢
((((0[,]1) × {𝑂}) ∈ (II Cn 𝐾) ∧ ((((0[,]1) × {𝑂})‘0) = 𝑂 ∧ (((0[,]1) × {𝑂})‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) |
| 89 | 21, 24, 27, 76, 88 | syl13anc 1374 |
. . 3
⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) |
| 90 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cvmlift3lem4 35327 |
. . . 4
⊢ ((𝜑 ∧ 𝑂 ∈ 𝑌) → ((𝐻‘𝑂) = 𝑃 ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))) |
| 91 | 6, 90 | mpdan 687 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑂) = 𝑃 ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))) |
| 92 | 89, 91 | mpbird 257 |
. 2
⊢ (𝜑 → (𝐻‘𝑂) = 𝑃) |
| 93 | | coeq2 5869 |
. . . . 5
⊢ (𝑓 = 𝐻 → (𝐹 ∘ 𝑓) = (𝐹 ∘ 𝐻)) |
| 94 | 93 | eqeq1d 2739 |
. . . 4
⊢ (𝑓 = 𝐻 → ((𝐹 ∘ 𝑓) = 𝐺 ↔ (𝐹 ∘ 𝐻) = 𝐺)) |
| 95 | | fveq1 6905 |
. . . . 5
⊢ (𝑓 = 𝐻 → (𝑓‘𝑂) = (𝐻‘𝑂)) |
| 96 | 95 | eqeq1d 2739 |
. . . 4
⊢ (𝑓 = 𝐻 → ((𝑓‘𝑂) = 𝑃 ↔ (𝐻‘𝑂) = 𝑃)) |
| 97 | 94, 96 | anbi12d 632 |
. . 3
⊢ (𝑓 = 𝐻 → (((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃) ↔ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃))) |
| 98 | 97 | rspcev 3622 |
. 2
⊢ ((𝐻 ∈ (𝐾 Cn 𝐶) ∧ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃)) → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) |
| 99 | 12, 13, 92, 98 | syl12anc 837 |
1
⊢ (𝜑 → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) |