Step | Hyp | Ref
| Expression |
1 | | htpyco2.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | | cntop1 21925 |
. . . 4
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
4 | | toptopon2 21603 |
. . 3
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
5 | 3, 4 | sylib 221 |
. 2
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
6 | | htpyco2.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ (𝐾 Cn 𝐿)) |
7 | | cnco 21951 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑃 ∈ (𝐾 Cn 𝐿)) → (𝑃 ∘ 𝐹) ∈ (𝐽 Cn 𝐿)) |
8 | 1, 6, 7 | syl2anc 588 |
. 2
⊢ (𝜑 → (𝑃 ∘ 𝐹) ∈ (𝐽 Cn 𝐿)) |
9 | | htpyco2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
10 | | cnco 21951 |
. . 3
⊢ ((𝐺 ∈ (𝐽 Cn 𝐾) ∧ 𝑃 ∈ (𝐾 Cn 𝐿)) → (𝑃 ∘ 𝐺) ∈ (𝐽 Cn 𝐿)) |
11 | 9, 6, 10 | syl2anc 588 |
. 2
⊢ (𝜑 → (𝑃 ∘ 𝐺) ∈ (𝐽 Cn 𝐿)) |
12 | 5, 1, 9 | htpycn 23659 |
. . . 4
⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾)) |
13 | | htpyco2.h |
. . . 4
⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) |
14 | 12, 13 | sseldd 3889 |
. . 3
⊢ (𝜑 → 𝐻 ∈ ((𝐽 ×t II) Cn 𝐾)) |
15 | | cnco 21951 |
. . 3
⊢ ((𝐻 ∈ ((𝐽 ×t II) Cn 𝐾) ∧ 𝑃 ∈ (𝐾 Cn 𝐿)) → (𝑃 ∘ 𝐻) ∈ ((𝐽 ×t II) Cn 𝐿)) |
16 | 14, 6, 15 | syl2anc 588 |
. 2
⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝐽 ×t II) Cn 𝐿)) |
17 | 5, 1, 9, 13 | htpyi 23660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠))) |
18 | 17 | simpld 499 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠𝐻0) = (𝐹‘𝑠)) |
19 | 18 | fveq2d 6655 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑃‘(𝑠𝐻0)) = (𝑃‘(𝐹‘𝑠))) |
20 | | iitopon 23565 |
. . . . . . 7
⊢ II ∈
(TopOn‘(0[,]1)) |
21 | | txtopon 22276 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ II ∈ (TopOn‘(0[,]1))) → (𝐽 ×t II) ∈
(TopOn‘(∪ 𝐽 × (0[,]1)))) |
22 | 5, 20, 21 | sylancl 590 |
. . . . . 6
⊢ (𝜑 → (𝐽 ×t II) ∈
(TopOn‘(∪ 𝐽 × (0[,]1)))) |
23 | | cntop2 21926 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
24 | 1, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
25 | | toptopon2 21603 |
. . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
26 | 24, 25 | sylib 221 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
27 | | cnf2 21934 |
. . . . . 6
⊢ (((𝐽 ×t II) ∈
(TopOn‘(∪ 𝐽 × (0[,]1))) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐻 ∈ ((𝐽 ×t II) Cn
𝐾)) → 𝐻:(∪
𝐽 ×
(0[,]1))⟶∪ 𝐾) |
28 | 22, 26, 14, 27 | syl3anc 1369 |
. . . . 5
⊢ (𝜑 → 𝐻:(∪ 𝐽 × (0[,]1))⟶∪ 𝐾) |
29 | | simpr 489 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → 𝑠 ∈ ∪ 𝐽) |
30 | | 0elunit 12886 |
. . . . . 6
⊢ 0 ∈
(0[,]1) |
31 | | opelxpi 5554 |
. . . . . 6
⊢ ((𝑠 ∈ ∪ 𝐽
∧ 0 ∈ (0[,]1)) → 〈𝑠, 0〉 ∈ (∪ 𝐽
× (0[,]1))) |
32 | 29, 30, 31 | sylancl 590 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → 〈𝑠, 0〉 ∈ (∪ 𝐽
× (0[,]1))) |
33 | | fvco3 6744 |
. . . . 5
⊢ ((𝐻:(∪
𝐽 ×
(0[,]1))⟶∪ 𝐾 ∧ 〈𝑠, 0〉 ∈ (∪ 𝐽
× (0[,]1))) → ((𝑃 ∘ 𝐻)‘〈𝑠, 0〉) = (𝑃‘(𝐻‘〈𝑠, 0〉))) |
34 | 28, 32, 33 | syl2an2r 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐻)‘〈𝑠, 0〉) = (𝑃‘(𝐻‘〈𝑠, 0〉))) |
35 | | df-ov 7146 |
. . . 4
⊢ (𝑠(𝑃 ∘ 𝐻)0) = ((𝑃 ∘ 𝐻)‘〈𝑠, 0〉) |
36 | | df-ov 7146 |
. . . . 5
⊢ (𝑠𝐻0) = (𝐻‘〈𝑠, 0〉) |
37 | 36 | fveq2i 6654 |
. . . 4
⊢ (𝑃‘(𝑠𝐻0)) = (𝑃‘(𝐻‘〈𝑠, 0〉)) |
38 | 34, 35, 37 | 3eqtr4g 2819 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)0) = (𝑃‘(𝑠𝐻0))) |
39 | | eqid 2759 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
40 | | eqid 2759 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
41 | 39, 40 | cnf 21931 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
42 | 1, 41 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:∪ 𝐽⟶∪ 𝐾) |
43 | | fvco3 6744 |
. . . 4
⊢ ((𝐹:∪
𝐽⟶∪ 𝐾
∧ 𝑠 ∈ ∪ 𝐽)
→ ((𝑃 ∘ 𝐹)‘𝑠) = (𝑃‘(𝐹‘𝑠))) |
44 | 42, 43 | sylan 584 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐹)‘𝑠) = (𝑃‘(𝐹‘𝑠))) |
45 | 19, 38, 44 | 3eqtr4d 2804 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)0) = ((𝑃 ∘ 𝐹)‘𝑠)) |
46 | 17 | simprd 500 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠𝐻1) = (𝐺‘𝑠)) |
47 | 46 | fveq2d 6655 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑃‘(𝑠𝐻1)) = (𝑃‘(𝐺‘𝑠))) |
48 | | 1elunit 12887 |
. . . . . 6
⊢ 1 ∈
(0[,]1) |
49 | | opelxpi 5554 |
. . . . . 6
⊢ ((𝑠 ∈ ∪ 𝐽
∧ 1 ∈ (0[,]1)) → 〈𝑠, 1〉 ∈ (∪ 𝐽
× (0[,]1))) |
50 | 29, 48, 49 | sylancl 590 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → 〈𝑠, 1〉 ∈ (∪ 𝐽
× (0[,]1))) |
51 | | fvco3 6744 |
. . . . 5
⊢ ((𝐻:(∪
𝐽 ×
(0[,]1))⟶∪ 𝐾 ∧ 〈𝑠, 1〉 ∈ (∪ 𝐽
× (0[,]1))) → ((𝑃 ∘ 𝐻)‘〈𝑠, 1〉) = (𝑃‘(𝐻‘〈𝑠, 1〉))) |
52 | 28, 50, 51 | syl2an2r 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐻)‘〈𝑠, 1〉) = (𝑃‘(𝐻‘〈𝑠, 1〉))) |
53 | | df-ov 7146 |
. . . 4
⊢ (𝑠(𝑃 ∘ 𝐻)1) = ((𝑃 ∘ 𝐻)‘〈𝑠, 1〉) |
54 | | df-ov 7146 |
. . . . 5
⊢ (𝑠𝐻1) = (𝐻‘〈𝑠, 1〉) |
55 | 54 | fveq2i 6654 |
. . . 4
⊢ (𝑃‘(𝑠𝐻1)) = (𝑃‘(𝐻‘〈𝑠, 1〉)) |
56 | 52, 53, 55 | 3eqtr4g 2819 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)1) = (𝑃‘(𝑠𝐻1))) |
57 | 39, 40 | cnf 21931 |
. . . . 5
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐺:∪ 𝐽⟶∪ 𝐾) |
58 | 9, 57 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:∪ 𝐽⟶∪ 𝐾) |
59 | | fvco3 6744 |
. . . 4
⊢ ((𝐺:∪
𝐽⟶∪ 𝐾
∧ 𝑠 ∈ ∪ 𝐽)
→ ((𝑃 ∘ 𝐺)‘𝑠) = (𝑃‘(𝐺‘𝑠))) |
60 | 58, 59 | sylan 584 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → ((𝑃 ∘ 𝐺)‘𝑠) = (𝑃‘(𝐺‘𝑠))) |
61 | 47, 56, 60 | 3eqtr4d 2804 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ 𝐽) → (𝑠(𝑃 ∘ 𝐻)1) = ((𝑃 ∘ 𝐺)‘𝑠)) |
62 | 5, 8, 11, 16, 45, 61 | ishtpyd 23661 |
1
⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(𝐽 Htpy 𝐿)(𝑃 ∘ 𝐺))) |