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
⊢ (𝜑 → 𝐾 ∈ SCon) |
5 | | cvmlift3.l |
. . 3
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
PCon) |
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 30562 |
. 2
⊢ (𝜑 → 𝐻 ∈ (𝐾 Cn 𝐶)) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cvmlift3lem5 30559 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) |
14 | | iitopon 22490 |
. . . . . 6
⊢ II ∈
(TopOn‘(0[,]1)) |
15 | 14 | a1i 11 |
. . . . 5
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
16 | | scontop 30464 |
. . . . . . 7
⊢ (𝐾 ∈ SCon → 𝐾 ∈ Top) |
17 | 4, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
18 | 2 | toptopon 20548 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
19 | 17, 18 | sylib 207 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
20 | | cnconst2 20897 |
. . . . 5
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑂 ∈ 𝑌) → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾)) |
21 | 15, 19, 6, 20 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾)) |
22 | | 0elunit 12161 |
. . . . 5
⊢ 0 ∈
(0[,]1) |
23 | | fvconst2g 6372 |
. . . . 5
⊢ ((𝑂 ∈ 𝑌 ∧ 0 ∈ (0[,]1)) → (((0[,]1)
× {𝑂})‘0) =
𝑂) |
24 | 6, 22, 23 | sylancl 693 |
. . . 4
⊢ (𝜑 → (((0[,]1) × {𝑂})‘0) = 𝑂) |
25 | | 1elunit 12162 |
. . . . 5
⊢ 1 ∈
(0[,]1) |
26 | | fvconst2g 6372 |
. . . . 5
⊢ ((𝑂 ∈ 𝑌 ∧ 1 ∈ (0[,]1)) → (((0[,]1)
× {𝑂})‘1) =
𝑂) |
27 | 6, 25, 26 | sylancl 693 |
. . . 4
⊢ (𝜑 → (((0[,]1) × {𝑂})‘1) = 𝑂) |
28 | 9 | sneqd 4137 |
. . . . . . . . 9
⊢ (𝜑 → {(𝐹‘𝑃)} = {(𝐺‘𝑂)}) |
29 | 28 | xpeq2d 5063 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]1) × {(𝐹‘𝑃)}) = ((0[,]1) × {(𝐺‘𝑂)})) |
30 | | cvmcn 30498 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
31 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
32 | 1, 31 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
33 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:𝐵⟶∪ 𝐽 → 𝐹 Fn 𝐵) |
34 | 3, 30, 32, 33 | 4syl 19 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐵) |
35 | | fcoconst 6307 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐵 ∧ 𝑃 ∈ 𝐵) → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)})) |
36 | 34, 8, 35 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)})) |
37 | 2, 31 | cnf 20860 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) |
38 | 7, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽) |
39 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐺:𝑌⟶∪ 𝐽 → 𝐺 Fn 𝑌) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn 𝑌) |
41 | | fcoconst 6307 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝑌 ∧ 𝑂 ∈ 𝑌) → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)})) |
42 | 40, 6, 41 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)})) |
43 | 29, 36, 42 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂}))) |
44 | | fvconst2g 6372 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝐵 ∧ 0 ∈ (0[,]1)) → (((0[,]1)
× {𝑃})‘0) =
𝑃) |
45 | 8, 22, 44 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → (((0[,]1) × {𝑃})‘0) = 𝑃) |
46 | | cvmtop1 30496 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
47 | 3, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Top) |
48 | 1 | toptopon 20548 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
49 | 47, 48 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
50 | | cnconst2 20897 |
. . . . . . . . 9
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐶 ∈ (TopOn‘𝐵) ∧ 𝑃 ∈ 𝐵) → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶)) |
51 | 15, 49, 8, 50 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶)) |
52 | | cvmtop2 30497 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top) |
53 | 3, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ Top) |
54 | 31 | toptopon 20548 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
55 | 53, 54 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
56 | 38, 6 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑂) ∈ ∪ 𝐽) |
57 | | cnconst2 20897 |
. . . . . . . . . . 11
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (𝐺‘𝑂) ∈ ∪ 𝐽)
→ ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽)) |
58 | 15, 55, 56, 57 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽)) |
59 | 42, 58 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽)) |
60 | | fvconst2g 6372 |
. . . . . . . . . . 11
⊢ (((𝐺‘𝑂) ∈ ∪ 𝐽 ∧ 0 ∈ (0[,]1)) →
(((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂)) |
61 | 56, 22, 60 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂)) |
62 | 42 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0) = (((0[,]1) × {(𝐺‘𝑂)})‘0)) |
63 | 61, 62, 9 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0)) |
64 | 1 | cvmlift 30535 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) |
65 | 3, 59, 8, 63, 64 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) |
66 | | coeq2 5202 |
. . . . . . . . . . 11
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ((0[,]1) × {𝑃}))) |
67 | 66 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ↔ (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})))) |
68 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝑔‘0) = (((0[,]1) × {𝑃})‘0)) |
69 | 68 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝑔‘0) = 𝑃 ↔ (((0[,]1) × {𝑃})‘0) = 𝑃)) |
70 | 67, 69 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑔 = ((0[,]1) × {𝑃}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃))) |
71 | 70 | riota2 6533 |
. . . . . . . 8
⊢
((((0[,]1) × {𝑃}) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃}))) |
72 | 51, 65, 71 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃}))) |
73 | 43, 45, 72 | mpbi2and 958 |
. . . . . 6
⊢ (𝜑 → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃})) |
74 | 73 | fveq1d 6105 |
. . . . 5
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = (((0[,]1) × {𝑃})‘1)) |
75 | | fvconst2g 6372 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐵 ∧ 1 ∈ (0[,]1)) → (((0[,]1)
× {𝑃})‘1) =
𝑃) |
76 | 8, 25, 75 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (((0[,]1) × {𝑃})‘1) = 𝑃) |
77 | 74, 76 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃) |
78 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘0) = (((0[,]1) × {𝑂})‘0)) |
79 | 78 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘0) = 𝑂 ↔ (((0[,]1) × {𝑂})‘0) = 𝑂)) |
80 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘1) = (((0[,]1) × {𝑂})‘1)) |
81 | 80 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘1) = 𝑂 ↔ (((0[,]1) × {𝑂})‘1) = 𝑂)) |
82 | | coeq2 5202 |
. . . . . . . . . . 11
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝐺 ∘ 𝑓) = (𝐺 ∘ ((0[,]1) × {𝑂}))) |
83 | 82 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})))) |
84 | 83 | anbi1d 737 |
. . . . . . . . 9
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))) |
85 | 84 | riotabidv 6513 |
. . . . . . . 8
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))) |
86 | 85 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1)) |
87 | 86 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃 ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) |
88 | 79, 81, 87 | 3anbi123d 1391 |
. . . . 5
⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃) ↔ ((((0[,]1) × {𝑂})‘0) = 𝑂 ∧ (((0[,]1) × {𝑂})‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))) |
89 | 88 | rspcev 3282 |
. . . 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) = 𝑃)) |
90 | 21, 24, 27, 77, 89 | syl13anc 1320 |
. . 3
⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) |
91 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cvmlift3lem4 30558 |
. . . 4
⊢ ((𝜑 ∧ 𝑂 ∈ 𝑌) → ((𝐻‘𝑂) = 𝑃 ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))) |
92 | 6, 91 | mpdan 699 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑂) = 𝑃 ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))) |
93 | 90, 92 | mpbird 246 |
. 2
⊢ (𝜑 → (𝐻‘𝑂) = 𝑃) |
94 | | coeq2 5202 |
. . . . 5
⊢ (𝑓 = 𝐻 → (𝐹 ∘ 𝑓) = (𝐹 ∘ 𝐻)) |
95 | 94 | eqeq1d 2612 |
. . . 4
⊢ (𝑓 = 𝐻 → ((𝐹 ∘ 𝑓) = 𝐺 ↔ (𝐹 ∘ 𝐻) = 𝐺)) |
96 | | fveq1 6102 |
. . . . 5
⊢ (𝑓 = 𝐻 → (𝑓‘𝑂) = (𝐻‘𝑂)) |
97 | 96 | eqeq1d 2612 |
. . . 4
⊢ (𝑓 = 𝐻 → ((𝑓‘𝑂) = 𝑃 ↔ (𝐻‘𝑂) = 𝑃)) |
98 | 95, 97 | anbi12d 743 |
. . 3
⊢ (𝑓 = 𝐻 → (((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃) ↔ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃))) |
99 | 98 | rspcev 3282 |
. 2
⊢ ((𝐻 ∈ (𝐾 Cn 𝐶) ∧ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃)) → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) |
100 | 12, 13, 93, 99 | syl12anc 1316 |
1
⊢ (𝜑 → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) |