| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | phtpyco2.f | . . 3
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) | 
| 2 |  | phtpyco2.p | . . 3
⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) | 
| 3 |  | cnco 23274 | . . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑃 ∈ (𝐽 Cn 𝐾)) → (𝑃 ∘ 𝐹) ∈ (II Cn 𝐾)) | 
| 4 | 1, 2, 3 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑃 ∘ 𝐹) ∈ (II Cn 𝐾)) | 
| 5 |  | phtpyco2.g | . . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) | 
| 6 |  | cnco 23274 | . . 3
⊢ ((𝐺 ∈ (II Cn 𝐽) ∧ 𝑃 ∈ (𝐽 Cn 𝐾)) → (𝑃 ∘ 𝐺) ∈ (II Cn 𝐾)) | 
| 7 | 5, 2, 6 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑃 ∘ 𝐺) ∈ (II Cn 𝐾)) | 
| 8 | 1, 5 | phtpyhtpy 25014 | . . . 4
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺)) | 
| 9 |  | phtpyco2.h | . . . 4
⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) | 
| 10 | 8, 9 | sseldd 3984 | . . 3
⊢ (𝜑 → 𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺)) | 
| 11 | 1, 5, 2, 10 | htpyco2 25011 | . 2
⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(II Htpy 𝐾)(𝑃 ∘ 𝐺))) | 
| 12 | 1, 5, 9 | phtpyi 25016 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1))) | 
| 13 | 12 | simpld 494 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘0)) | 
| 14 | 13 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑃‘(0𝐻𝑠)) = (𝑃‘(𝐹‘0))) | 
| 15 |  | iitopon 24905 | . . . . . . 7
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 16 |  | txtopon 23599 | . . . . . . 7
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1)))) | 
| 17 | 15, 15, 16 | mp2an 692 | . . . . . 6
⊢ (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1))) | 
| 18 |  | cntop2 23249 | . . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) | 
| 19 | 1, 18 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 20 |  | toptopon2 22924 | . . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 21 | 19, 20 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 22 | 1, 5 | phtpycn 25015 | . . . . . . 7
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ ((II ×t II) Cn
𝐽)) | 
| 23 | 22, 9 | sseldd 3984 | . . . . . 6
⊢ (𝜑 → 𝐻 ∈ ((II ×t II) Cn
𝐽)) | 
| 24 |  | cnf2 23257 | . . . . . 6
⊢ (((II
×t II) ∈ (TopOn‘((0[,]1) × (0[,]1))) ∧
𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐻 ∈ ((II
×t II) Cn 𝐽)) → 𝐻:((0[,]1) × (0[,]1))⟶∪ 𝐽) | 
| 25 | 17, 21, 23, 24 | mp3an2i 1468 | . . . . 5
⊢ (𝜑 → 𝐻:((0[,]1) × (0[,]1))⟶∪ 𝐽) | 
| 26 |  | 0elunit 13509 | . . . . . 6
⊢ 0 ∈
(0[,]1) | 
| 27 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1)) | 
| 28 |  | opelxpi 5722 | . . . . . 6
⊢ ((0
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → 〈0, 𝑠〉 ∈ ((0[,]1) ×
(0[,]1))) | 
| 29 | 26, 27, 28 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 〈0, 𝑠〉 ∈ ((0[,]1) ×
(0[,]1))) | 
| 30 |  | fvco3 7008 | . . . . 5
⊢ ((𝐻:((0[,]1) ×
(0[,]1))⟶∪ 𝐽 ∧ 〈0, 𝑠〉 ∈ ((0[,]1) × (0[,]1)))
→ ((𝑃 ∘ 𝐻)‘〈0, 𝑠〉) = (𝑃‘(𝐻‘〈0, 𝑠〉))) | 
| 31 | 25, 29, 30 | syl2an2r 685 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝑃 ∘ 𝐻)‘〈0, 𝑠〉) = (𝑃‘(𝐻‘〈0, 𝑠〉))) | 
| 32 |  | df-ov 7434 | . . . 4
⊢ (0(𝑃 ∘ 𝐻)𝑠) = ((𝑃 ∘ 𝐻)‘〈0, 𝑠〉) | 
| 33 |  | df-ov 7434 | . . . . 5
⊢ (0𝐻𝑠) = (𝐻‘〈0, 𝑠〉) | 
| 34 | 33 | fveq2i 6909 | . . . 4
⊢ (𝑃‘(0𝐻𝑠)) = (𝑃‘(𝐻‘〈0, 𝑠〉)) | 
| 35 | 31, 32, 34 | 3eqtr4g 2802 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0(𝑃 ∘ 𝐻)𝑠) = (𝑃‘(0𝐻𝑠))) | 
| 36 |  | iiuni 24907 | . . . . . . 7
⊢ (0[,]1) =
∪ II | 
| 37 |  | eqid 2737 | . . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 38 | 36, 37 | cnf 23254 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶∪
𝐽) | 
| 39 | 1, 38 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐹:(0[,]1)⟶∪
𝐽) | 
| 40 | 39 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝐹:(0[,]1)⟶∪
𝐽) | 
| 41 |  | fvco3 7008 | . . . 4
⊢ ((𝐹:(0[,]1)⟶∪ 𝐽
∧ 0 ∈ (0[,]1)) → ((𝑃 ∘ 𝐹)‘0) = (𝑃‘(𝐹‘0))) | 
| 42 | 40, 26, 41 | sylancl 586 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝑃 ∘ 𝐹)‘0) = (𝑃‘(𝐹‘0))) | 
| 43 | 14, 35, 42 | 3eqtr4d 2787 | . 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0(𝑃 ∘ 𝐻)𝑠) = ((𝑃 ∘ 𝐹)‘0)) | 
| 44 | 12 | simprd 495 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘1)) | 
| 45 | 44 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑃‘(1𝐻𝑠)) = (𝑃‘(𝐹‘1))) | 
| 46 |  | 1elunit 13510 | . . . . . 6
⊢ 1 ∈
(0[,]1) | 
| 47 |  | opelxpi 5722 | . . . . . 6
⊢ ((1
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → 〈1, 𝑠〉 ∈ ((0[,]1) ×
(0[,]1))) | 
| 48 | 46, 27, 47 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 〈1, 𝑠〉 ∈ ((0[,]1) ×
(0[,]1))) | 
| 49 |  | fvco3 7008 | . . . . 5
⊢ ((𝐻:((0[,]1) ×
(0[,]1))⟶∪ 𝐽 ∧ 〈1, 𝑠〉 ∈ ((0[,]1) × (0[,]1)))
→ ((𝑃 ∘ 𝐻)‘〈1, 𝑠〉) = (𝑃‘(𝐻‘〈1, 𝑠〉))) | 
| 50 | 25, 48, 49 | syl2an2r 685 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝑃 ∘ 𝐻)‘〈1, 𝑠〉) = (𝑃‘(𝐻‘〈1, 𝑠〉))) | 
| 51 |  | df-ov 7434 | . . . 4
⊢ (1(𝑃 ∘ 𝐻)𝑠) = ((𝑃 ∘ 𝐻)‘〈1, 𝑠〉) | 
| 52 |  | df-ov 7434 | . . . . 5
⊢ (1𝐻𝑠) = (𝐻‘〈1, 𝑠〉) | 
| 53 | 52 | fveq2i 6909 | . . . 4
⊢ (𝑃‘(1𝐻𝑠)) = (𝑃‘(𝐻‘〈1, 𝑠〉)) | 
| 54 | 50, 51, 53 | 3eqtr4g 2802 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1(𝑃 ∘ 𝐻)𝑠) = (𝑃‘(1𝐻𝑠))) | 
| 55 |  | fvco3 7008 | . . . 4
⊢ ((𝐹:(0[,]1)⟶∪ 𝐽
∧ 1 ∈ (0[,]1)) → ((𝑃 ∘ 𝐹)‘1) = (𝑃‘(𝐹‘1))) | 
| 56 | 40, 46, 55 | sylancl 586 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝑃 ∘ 𝐹)‘1) = (𝑃‘(𝐹‘1))) | 
| 57 | 45, 54, 56 | 3eqtr4d 2787 | . 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1(𝑃 ∘ 𝐻)𝑠) = ((𝑃 ∘ 𝐹)‘1)) | 
| 58 | 4, 7, 11, 43, 57 | isphtpyd 25018 | 1
⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺))) |