Step | Hyp | Ref
| Expression |
1 | | htpyco1.j |
. 2
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | htpyco1.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) |
3 | | htpyco1.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐾 Cn 𝐿)) |
4 | | cnco 21070 |
. . 3
⊢ ((𝑃 ∈ (𝐽 Cn 𝐾) ∧ 𝐹 ∈ (𝐾 Cn 𝐿)) → (𝐹 ∘ 𝑃) ∈ (𝐽 Cn 𝐿)) |
5 | 2, 3, 4 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝑃) ∈ (𝐽 Cn 𝐿)) |
6 | | htpyco1.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐿)) |
7 | | cnco 21070 |
. . 3
⊢ ((𝑃 ∈ (𝐽 Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐿)) → (𝐺 ∘ 𝑃) ∈ (𝐽 Cn 𝐿)) |
8 | 2, 6, 7 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝑃) ∈ (𝐽 Cn 𝐿)) |
9 | | htpyco1.n |
. . 3
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ ((𝑃‘𝑥)𝐻𝑦)) |
10 | | iitopon 22682 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
12 | 1, 11 | cnmpt1st 21471 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((𝐽 ×t II) Cn 𝐽)) |
13 | 1, 11, 12, 2 | cnmpt21f 21475 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ (𝑃‘𝑥)) ∈ ((𝐽 ×t II) Cn 𝐾)) |
14 | 1, 11 | cnmpt2nd 21472 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((𝐽 ×t II) Cn
II)) |
15 | | cntop2 21045 |
. . . . . . . 8
⊢ (𝑃 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
16 | 2, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
17 | | eqid 2622 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
18 | 17 | toptopon 20722 |
. . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
19 | 16, 18 | sylib 208 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
20 | 19, 3, 6 | htpycn 22772 |
. . . . 5
⊢ (𝜑 → (𝐹(𝐾 Htpy 𝐿)𝐺) ⊆ ((𝐾 ×t II) Cn 𝐿)) |
21 | | htpyco1.h |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐾 Htpy 𝐿)𝐺)) |
22 | 20, 21 | sseldd 3604 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ ((𝐾 ×t II) Cn 𝐿)) |
23 | 1, 11, 13, 14, 22 | cnmpt22f 21478 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ ((𝑃‘𝑥)𝐻𝑦)) ∈ ((𝐽 ×t II) Cn 𝐿)) |
24 | 9, 23 | syl5eqel 2705 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝐽 ×t II) Cn 𝐿)) |
25 | | cnf2 21053 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑃 ∈ (𝐽 Cn 𝐾)) → 𝑃:𝑋⟶∪ 𝐾) |
26 | 1, 19, 2, 25 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → 𝑃:𝑋⟶∪ 𝐾) |
27 | 26 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑃‘𝑠) ∈ ∪ 𝐾) |
28 | 19, 3, 6, 21 | htpyi 22773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑃‘𝑠) ∈ ∪ 𝐾) → (((𝑃‘𝑠)𝐻0) = (𝐹‘(𝑃‘𝑠)) ∧ ((𝑃‘𝑠)𝐻1) = (𝐺‘(𝑃‘𝑠)))) |
29 | 27, 28 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (((𝑃‘𝑠)𝐻0) = (𝐹‘(𝑃‘𝑠)) ∧ ((𝑃‘𝑠)𝐻1) = (𝐺‘(𝑃‘𝑠)))) |
30 | 29 | simpld 475 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝑃‘𝑠)𝐻0) = (𝐹‘(𝑃‘𝑠))) |
31 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → 𝑠 ∈ 𝑋) |
32 | | 0elunit 12290 |
. . . 4
⊢ 0 ∈
(0[,]1) |
33 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑠 → (𝑃‘𝑥) = (𝑃‘𝑠)) |
34 | | id 22 |
. . . . . 6
⊢ (𝑦 = 0 → 𝑦 = 0) |
35 | 33, 34 | oveqan12d 6669 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → ((𝑃‘𝑥)𝐻𝑦) = ((𝑃‘𝑠)𝐻0)) |
36 | | ovex 6678 |
. . . . 5
⊢ ((𝑃‘𝑠)𝐻0) ∈ V |
37 | 35, 9, 36 | ovmpt2a 6791 |
. . . 4
⊢ ((𝑠 ∈ 𝑋 ∧ 0 ∈ (0[,]1)) → (𝑠𝑁0) = ((𝑃‘𝑠)𝐻0)) |
38 | 31, 32, 37 | sylancl 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁0) = ((𝑃‘𝑠)𝐻0)) |
39 | | fvco3 6275 |
. . . 4
⊢ ((𝑃:𝑋⟶∪ 𝐾 ∧ 𝑠 ∈ 𝑋) → ((𝐹 ∘ 𝑃)‘𝑠) = (𝐹‘(𝑃‘𝑠))) |
40 | 26, 39 | sylan 488 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝐹 ∘ 𝑃)‘𝑠) = (𝐹‘(𝑃‘𝑠))) |
41 | 30, 38, 40 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁0) = ((𝐹 ∘ 𝑃)‘𝑠)) |
42 | 29 | simprd 479 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝑃‘𝑠)𝐻1) = (𝐺‘(𝑃‘𝑠))) |
43 | | 1elunit 12291 |
. . . 4
⊢ 1 ∈
(0[,]1) |
44 | | id 22 |
. . . . . 6
⊢ (𝑦 = 1 → 𝑦 = 1) |
45 | 33, 44 | oveqan12d 6669 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((𝑃‘𝑥)𝐻𝑦) = ((𝑃‘𝑠)𝐻1)) |
46 | | ovex 6678 |
. . . . 5
⊢ ((𝑃‘𝑠)𝐻1) ∈ V |
47 | 45, 9, 46 | ovmpt2a 6791 |
. . . 4
⊢ ((𝑠 ∈ 𝑋 ∧ 1 ∈ (0[,]1)) → (𝑠𝑁1) = ((𝑃‘𝑠)𝐻1)) |
48 | 31, 43, 47 | sylancl 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁1) = ((𝑃‘𝑠)𝐻1)) |
49 | | fvco3 6275 |
. . . 4
⊢ ((𝑃:𝑋⟶∪ 𝐾 ∧ 𝑠 ∈ 𝑋) → ((𝐺 ∘ 𝑃)‘𝑠) = (𝐺‘(𝑃‘𝑠))) |
50 | 26, 49 | sylan 488 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝐺 ∘ 𝑃)‘𝑠) = (𝐺‘(𝑃‘𝑠))) |
51 | 42, 48, 50 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁1) = ((𝐺 ∘ 𝑃)‘𝑠)) |
52 | 1, 5, 8, 24, 41, 51 | ishtpyd 22774 |
1
⊢ (𝜑 → 𝑁 ∈ ((𝐹 ∘ 𝑃)(𝐽 Htpy 𝐿)(𝐺 ∘ 𝑃))) |