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