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 32861 |
. 2
⊢ (𝜑 → 𝐻 ∈ (𝐾 Cn 𝐶)) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cvmlift3lem5 32858 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) |
14 | | iitopon 23633 |
. . . . . 6
⊢ II ∈
(TopOn‘(0[,]1)) |
15 | 14 | a1i 11 |
. . . . 5
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
16 | | sconntop 32763 |
. . . . . . 7
⊢ (𝐾 ∈ SConn → 𝐾 ∈ Top) |
17 | 4, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
18 | 2 | toptopon 21670 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
19 | 17, 18 | sylib 221 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
20 | | cnconst2 22036 |
. . . . 5
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑂 ∈ 𝑌) → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾)) |
21 | 15, 19, 6, 20 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾)) |
22 | | 0elunit 12945 |
. . . . 5
⊢ 0 ∈
(0[,]1) |
23 | | fvconst2g 6976 |
. . . . 5
⊢ ((𝑂 ∈ 𝑌 ∧ 0 ∈ (0[,]1)) → (((0[,]1)
× {𝑂})‘0) =
𝑂) |
24 | 6, 22, 23 | sylancl 589 |
. . . 4
⊢ (𝜑 → (((0[,]1) × {𝑂})‘0) = 𝑂) |
25 | | 1elunit 12946 |
. . . . 5
⊢ 1 ∈
(0[,]1) |
26 | | fvconst2g 6976 |
. . . . 5
⊢ ((𝑂 ∈ 𝑌 ∧ 1 ∈ (0[,]1)) → (((0[,]1)
× {𝑂})‘1) =
𝑂) |
27 | 6, 25, 26 | sylancl 589 |
. . . 4
⊢ (𝜑 → (((0[,]1) × {𝑂})‘1) = 𝑂) |
28 | 9 | sneqd 4528 |
. . . . . . . . 9
⊢ (𝜑 → {(𝐹‘𝑃)} = {(𝐺‘𝑂)}) |
29 | 28 | xpeq2d 5555 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]1) × {(𝐹‘𝑃)}) = ((0[,]1) × {(𝐺‘𝑂)})) |
30 | | cvmcn 32797 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
31 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
32 | 1, 31 | cnf 21999 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
33 | | ffn 6504 |
. . . . . . . . . 10
⊢ (𝐹:𝐵⟶∪ 𝐽 → 𝐹 Fn 𝐵) |
34 | 3, 30, 32, 33 | 4syl 19 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐵) |
35 | | fcoconst 6908 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐵 ∧ 𝑃 ∈ 𝐵) → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)})) |
36 | 34, 8, 35 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)})) |
37 | 2, 31 | cnf 21999 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) |
38 | 7, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽) |
39 | 38 | ffnd 6505 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn 𝑌) |
40 | | fcoconst 6908 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝑌 ∧ 𝑂 ∈ 𝑌) → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)})) |
41 | 39, 6, 40 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)})) |
42 | 29, 36, 41 | 3eqtr4d 2783 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂}))) |
43 | | fvconst2g 6976 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝐵 ∧ 0 ∈ (0[,]1)) → (((0[,]1)
× {𝑃})‘0) =
𝑃) |
44 | 8, 22, 43 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → (((0[,]1) × {𝑃})‘0) = 𝑃) |
45 | | cvmtop1 32795 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
46 | 3, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Top) |
47 | 1 | toptopon 21670 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
48 | 46, 47 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
49 | | cnconst2 22036 |
. . . . . . . . 9
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐶 ∈ (TopOn‘𝐵) ∧ 𝑃 ∈ 𝐵) → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶)) |
50 | 15, 48, 8, 49 | syl3anc 1372 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶)) |
51 | | cvmtop2 32796 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top) |
52 | 3, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ Top) |
53 | 31 | toptopon 21670 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
54 | 52, 53 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
55 | 38, 6 | ffvelrnd 6864 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑂) ∈ ∪ 𝐽) |
56 | | cnconst2 22036 |
. . . . . . . . . . 11
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (𝐺‘𝑂) ∈ ∪ 𝐽)
→ ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽)) |
57 | 15, 54, 55, 56 | syl3anc 1372 |
. . . . . . . . . 10
⊢ (𝜑 → ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽)) |
58 | 41, 57 | eqeltrd 2833 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽)) |
59 | | fvconst2g 6976 |
. . . . . . . . . . 11
⊢ (((𝐺‘𝑂) ∈ ∪ 𝐽 ∧ 0 ∈ (0[,]1)) →
(((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂)) |
60 | 55, 22, 59 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝜑 → (((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂)) |
61 | 41 | fveq1d 6678 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0) = (((0[,]1) × {(𝐺‘𝑂)})‘0)) |
62 | 60, 61, 9 | 3eqtr4rd 2784 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0)) |
63 | 1 | cvmlift 32834 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) |
64 | 3, 58, 8, 62, 63 | syl22anc 838 |
. . . . . . . 8
⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) |
65 | | coeq2 5701 |
. . . . . . . . . . 11
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ((0[,]1) × {𝑃}))) |
66 | 65 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ↔ (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})))) |
67 | | fveq1 6675 |
. . . . . . . . . . 11
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝑔‘0) = (((0[,]1) × {𝑃})‘0)) |
68 | 67 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝑔‘0) = 𝑃 ↔ (((0[,]1) × {𝑃})‘0) = 𝑃)) |
69 | 66, 68 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃))) |
70 | 69 | riota2 7155 |
. . . . . . . 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 587 |
. . . . . . 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 6678 |
. . . . 5
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = (((0[,]1) × {𝑃})‘1)) |
74 | | fvconst2g 6976 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐵 ∧ 1 ∈ (0[,]1)) → (((0[,]1)
× {𝑃})‘1) =
𝑃) |
75 | 8, 25, 74 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (((0[,]1) × {𝑃})‘1) = 𝑃) |
76 | 73, 75 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃) |
77 | | fveq1 6675 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘0) = (((0[,]1) × {𝑂})‘0)) |
78 | 77 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘0) = 𝑂 ↔ (((0[,]1) × {𝑂})‘0) = 𝑂)) |
79 | | fveq1 6675 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘1) = (((0[,]1) × {𝑂})‘1)) |
80 | 79 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘1) = 𝑂 ↔ (((0[,]1) × {𝑂})‘1) = 𝑂)) |
81 | | coeq2 5701 |
. . . . . . . . . . 11
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝐺 ∘ 𝑓) = (𝐺 ∘ ((0[,]1) × {𝑂}))) |
82 | 81 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})))) |
83 | 82 | anbi1d 633 |
. . . . . . . . 9
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))) |
84 | 83 | riotabidv 7131 |
. . . . . . . 8
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))) |
85 | 84 | fveq1d 6678 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1)) |
86 | 85 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃 ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) |
87 | 78, 80, 86 | 3anbi123d 1437 |
. . . . 5
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃) ↔ ((((0[,]1) × {𝑂})‘0) = 𝑂 ∧ (((0[,]1) × {𝑂})‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))) |
88 | 87 | rspcev 3526 |
. . . 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 1373 |
. . 3
⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) |
90 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cvmlift3lem4 32857 |
. . . 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 260 |
. 2
⊢ (𝜑 → (𝐻‘𝑂) = 𝑃) |
93 | | coeq2 5701 |
. . . . 5
⊢ (𝑓 = 𝐻 → (𝐹 ∘ 𝑓) = (𝐹 ∘ 𝐻)) |
94 | 93 | eqeq1d 2740 |
. . . 4
⊢ (𝑓 = 𝐻 → ((𝐹 ∘ 𝑓) = 𝐺 ↔ (𝐹 ∘ 𝐻) = 𝐺)) |
95 | | fveq1 6675 |
. . . . 5
⊢ (𝑓 = 𝐻 → (𝑓‘𝑂) = (𝐻‘𝑂)) |
96 | 95 | eqeq1d 2740 |
. . . 4
⊢ (𝑓 = 𝐻 → ((𝑓‘𝑂) = 𝑃 ↔ (𝐻‘𝑂) = 𝑃)) |
97 | 94, 96 | anbi12d 634 |
. . 3
⊢ (𝑓 = 𝐻 → (((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃) ↔ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃))) |
98 | 97 | rspcev 3526 |
. 2
⊢ ((𝐻 ∈ (𝐾 Cn 𝐶) ∧ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃)) → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) |
99 | 12, 13, 92, 98 | syl12anc 836 |
1
⊢ (𝜑 → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) |