Step | Hyp | Ref
| Expression |
1 | | htpyco2.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | | cntop1 20854 |
. . . 4
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
4 | | eqid 2610 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | 4 | toptopon 20548 |
. . 3
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
6 | 3, 5 | sylib 207 |
. 2
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
7 | | htpyco2.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ (𝐾 Cn 𝐿)) |
8 | | cnco 20880 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑃 ∈ (𝐾 Cn 𝐿)) → (𝑃 ∘ 𝐹) ∈ (𝐽 Cn 𝐿)) |
9 | 1, 7, 8 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑃 ∘ 𝐹) ∈ (𝐽 Cn 𝐿)) |
10 | | htpyco2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
11 | | cnco 20880 |
. . 3
⊢ ((𝐺 ∈ (𝐽 Cn 𝐾) ∧ 𝑃 ∈ (𝐾 Cn 𝐿)) → (𝑃 ∘ 𝐺) ∈ (𝐽 Cn 𝐿)) |
12 | 10, 7, 11 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑃 ∘ 𝐺) ∈ (𝐽 Cn 𝐿)) |
13 | 6, 1, 10 | htpycn 22580 |
. . . 4
⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾)) |
14 | | htpyco2.h |
. . . 4
⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) |
15 | 13, 14 | sseldd 3569 |
. . 3
⊢ (𝜑 → 𝐻 ∈ ((𝐽 ×t II) Cn 𝐾)) |
16 | | cnco 20880 |
. . 3
⊢ ((𝐻 ∈ ((𝐽 ×t II) Cn 𝐾) ∧ 𝑃 ∈ (𝐾 Cn 𝐿)) → (𝑃 ∘ 𝐻) ∈ ((𝐽 ×t II) Cn 𝐿)) |
17 | 15, 7, 16 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝐽 ×t II) Cn 𝐿)) |
18 | 6, 1, 10, 14 | htpyi 22581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠))) |
19 | 18 | simpld 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠𝐻0) = (𝐹‘𝑠)) |
20 | 19 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑃‘(𝑠𝐻0)) = (𝑃‘(𝐹‘𝑠))) |
21 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → 𝑠 ∈ ∪ 𝐽) |
22 | | 0elunit 12161 |
. . . . . 6
⊢ 0 ∈
(0[,]1) |
23 | | opelxpi 5072 |
. . . . . 6
⊢ ((𝑠 ∈ ∪ 𝐽
∧ 0 ∈ (0[,]1)) → 〈𝑠, 0〉 ∈ (∪ 𝐽
× (0[,]1))) |
24 | 21, 22, 23 | sylancl 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → 〈𝑠, 0〉 ∈ (∪ 𝐽
× (0[,]1))) |
25 | | iitopon 22490 |
. . . . . . . 8
⊢ II ∈
(TopOn‘(0[,]1)) |
26 | | txtopon 21204 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ II ∈ (TopOn‘(0[,]1))) → (𝐽 ×t II) ∈
(TopOn‘(∪ 𝐽 × (0[,]1)))) |
27 | 6, 25, 26 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → (𝐽 ×t II) ∈
(TopOn‘(∪ 𝐽 × (0[,]1)))) |
28 | | cntop2 20855 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
29 | 1, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Top) |
30 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ 𝐾 =
∪ 𝐾 |
31 | 30 | toptopon 20548 |
. . . . . . . 8
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
32 | 29, 31 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
33 | | cnf2 20863 |
. . . . . . 7
⊢ (((𝐽 ×t II) ∈
(TopOn‘(∪ 𝐽 × (0[,]1))) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐻 ∈ ((𝐽 ×t II) Cn
𝐾)) → 𝐻:(∪
𝐽 ×
(0[,]1))⟶∪ 𝐾) |
34 | 27, 32, 15, 33 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 𝐻:(∪ 𝐽 × (0[,]1))⟶∪ 𝐾) |
35 | | fvco3 6185 |
. . . . . 6
⊢ ((𝐻:(∪
𝐽 ×
(0[,]1))⟶∪ 𝐾 ∧ 〈𝑠, 0〉 ∈ (∪ 𝐽
× (0[,]1))) → ((𝑃 ∘ 𝐻)‘〈𝑠, 0〉) = (𝑃‘(𝐻‘〈𝑠, 0〉))) |
36 | 34, 35 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 〈𝑠, 0〉 ∈ (∪ 𝐽
× (0[,]1))) → ((𝑃 ∘ 𝐻)‘〈𝑠, 0〉) = (𝑃‘(𝐻‘〈𝑠, 0〉))) |
37 | 24, 36 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐻)‘〈𝑠, 0〉) = (𝑃‘(𝐻‘〈𝑠, 0〉))) |
38 | | df-ov 6552 |
. . . 4
⊢ (𝑠(𝑃 ∘ 𝐻)0) = ((𝑃 ∘ 𝐻)‘〈𝑠, 0〉) |
39 | | df-ov 6552 |
. . . . 5
⊢ (𝑠𝐻0) = (𝐻‘〈𝑠, 0〉) |
40 | 39 | fveq2i 6106 |
. . . 4
⊢ (𝑃‘(𝑠𝐻0)) = (𝑃‘(𝐻‘〈𝑠, 0〉)) |
41 | 37, 38, 40 | 3eqtr4g 2669 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)0) = (𝑃‘(𝑠𝐻0))) |
42 | 4, 30 | cnf 20860 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
43 | 1, 42 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:∪ 𝐽⟶∪ 𝐾) |
44 | | fvco3 6185 |
. . . 4
⊢ ((𝐹:∪
𝐽⟶∪ 𝐾
∧ 𝑠 ∈ ∪ 𝐽)
→ ((𝑃 ∘ 𝐹)‘𝑠) = (𝑃‘(𝐹‘𝑠))) |
45 | 43, 44 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐹)‘𝑠) = (𝑃‘(𝐹‘𝑠))) |
46 | 20, 41, 45 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)0) = ((𝑃 ∘ 𝐹)‘𝑠)) |
47 | 18 | simprd 478 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠𝐻1) = (𝐺‘𝑠)) |
48 | 47 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑃‘(𝑠𝐻1)) = (𝑃‘(𝐺‘𝑠))) |
49 | | 1elunit 12162 |
. . . . . 6
⊢ 1 ∈
(0[,]1) |
50 | | opelxpi 5072 |
. . . . . 6
⊢ ((𝑠 ∈ ∪ 𝐽
∧ 1 ∈ (0[,]1)) → 〈𝑠, 1〉 ∈ (∪ 𝐽
× (0[,]1))) |
51 | 21, 49, 50 | sylancl 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → 〈𝑠, 1〉 ∈ (∪ 𝐽
× (0[,]1))) |
52 | | fvco3 6185 |
. . . . . 6
⊢ ((𝐻:(∪
𝐽 ×
(0[,]1))⟶∪ 𝐾 ∧ 〈𝑠, 1〉 ∈ (∪ 𝐽
× (0[,]1))) → ((𝑃 ∘ 𝐻)‘〈𝑠, 1〉) = (𝑃‘(𝐻‘〈𝑠, 1〉))) |
53 | 34, 52 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 〈𝑠, 1〉 ∈ (∪ 𝐽
× (0[,]1))) → ((𝑃 ∘ 𝐻)‘〈𝑠, 1〉) = (𝑃‘(𝐻‘〈𝑠, 1〉))) |
54 | 51, 53 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐻)‘〈𝑠, 1〉) = (𝑃‘(𝐻‘〈𝑠, 1〉))) |
55 | | df-ov 6552 |
. . . 4
⊢ (𝑠(𝑃 ∘ 𝐻)1) = ((𝑃 ∘ 𝐻)‘〈𝑠, 1〉) |
56 | | df-ov 6552 |
. . . . 5
⊢ (𝑠𝐻1) = (𝐻‘〈𝑠, 1〉) |
57 | 56 | fveq2i 6106 |
. . . 4
⊢ (𝑃‘(𝑠𝐻1)) = (𝑃‘(𝐻‘〈𝑠, 1〉)) |
58 | 54, 55, 57 | 3eqtr4g 2669 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)1) = (𝑃‘(𝑠𝐻1))) |
59 | 4, 30 | cnf 20860 |
. . . . 5
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐺:∪ 𝐽⟶∪ 𝐾) |
60 | 10, 59 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:∪ 𝐽⟶∪ 𝐾) |
61 | | fvco3 6185 |
. . . 4
⊢ ((𝐺:∪
𝐽⟶∪ 𝐾
∧ 𝑠 ∈ ∪ 𝐽)
→ ((𝑃 ∘ 𝐺)‘𝑠) = (𝑃‘(𝐺‘𝑠))) |
62 | 60, 61 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐺)‘𝑠) = (𝑃‘(𝐺‘𝑠))) |
63 | 48, 58, 62 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)1) = ((𝑃 ∘ 𝐺)‘𝑠)) |
64 | 6, 9, 12, 17, 46, 63 | ishtpyd 22582 |
1
⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(𝐽 Htpy 𝐿)(𝑃 ∘ 𝐺))) |