Step | Hyp | Ref
| Expression |
1 | | htpycc.2 |
. 2
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | htpycc.4 |
. 2
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
3 | | htpycc.6 |
. 2
⊢ (𝜑 → 𝐻 ∈ (𝐽 Cn 𝐾)) |
4 | | htpycc.1 |
. . 3
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1)))) |
5 | | iitopon 22490 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
6 | 5 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
7 | | eqid 2610 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
8 | | eqid 2610 |
. . . . 5
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
9 | | eqid 2610 |
. . . . 5
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
10 | | dfii2 22493 |
. . . . 5
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
11 | | 0red 9920 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ) |
12 | | 1red 9934 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
13 | | halfre 11123 |
. . . . . . 7
⊢ (1 / 2)
∈ ℝ |
14 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
15 | | halfgt0 11125 |
. . . . . . . 8
⊢ 0 < (1
/ 2) |
16 | 14, 13, 15 | ltleii 10039 |
. . . . . . 7
⊢ 0 ≤ (1
/ 2) |
17 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
18 | | halflt1 11127 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
19 | 13, 17, 18 | ltleii 10039 |
. . . . . . 7
⊢ (1 / 2)
≤ 1 |
20 | 14, 17 | elicc2i 12110 |
. . . . . . 7
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
21 | 13, 16, 19, 20 | mpbir3an 1237 |
. . . . . 6
⊢ (1 / 2)
∈ (0[,]1) |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → (1 / 2) ∈
(0[,]1)) |
23 | | htpycc.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
24 | | htpycc.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) |
25 | 1, 2, 23, 24 | htpyi 22581 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝑠𝐿0) = (𝐹‘𝑠) ∧ (𝑠𝐿1) = (𝐺‘𝑠))) |
26 | 25 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐿1) = (𝐺‘𝑠)) |
27 | | htpycc.8 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (𝐺(𝐽 Htpy 𝐾)𝐻)) |
28 | 1, 23, 3, 27 | htpyi 22581 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝑠𝑀0) = (𝐺‘𝑠) ∧ (𝑠𝑀1) = (𝐻‘𝑠))) |
29 | 28 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑀0) = (𝐺‘𝑠)) |
30 | 26, 29 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐿1) = (𝑠𝑀0)) |
31 | 30 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑠 ∈ 𝑋 (𝑠𝐿1) = (𝑠𝑀0)) |
32 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → (𝑠𝐿1) = (𝑥𝐿1)) |
33 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → (𝑠𝑀0) = (𝑥𝑀0)) |
34 | 32, 33 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑠 = 𝑥 → ((𝑠𝐿1) = (𝑠𝑀0) ↔ (𝑥𝐿1) = (𝑥𝑀0))) |
35 | 34 | rspccva 3281 |
. . . . . . . 8
⊢
((∀𝑠 ∈
𝑋 (𝑠𝐿1) = (𝑠𝑀0) ∧ 𝑥 ∈ 𝑋) → (𝑥𝐿1) = (𝑥𝑀0)) |
36 | 31, 35 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐿1) = (𝑥𝑀0)) |
37 | 36 | adantrl 748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝐿1) = (𝑥𝑀0)) |
38 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → 𝑦 = (1 / 2)) |
39 | 38 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (2 · 𝑦) = (2 · (1 / 2))) |
40 | | 2cn 10968 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
41 | | 2ne0 10990 |
. . . . . . . . 9
⊢ 2 ≠
0 |
42 | 40, 41 | recidi 10635 |
. . . . . . . 8
⊢ (2
· (1 / 2)) = 1 |
43 | 39, 42 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (2 · 𝑦) = 1) |
44 | 43 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝐿(2 · 𝑦)) = (𝑥𝐿1)) |
45 | 43 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → ((2 · 𝑦) − 1) = (1 −
1)) |
46 | | 1m1e0 10966 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
47 | 45, 46 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → ((2 · 𝑦) − 1) = 0) |
48 | 47 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝑀((2 · 𝑦) − 1)) = (𝑥𝑀0)) |
49 | 37, 44, 48 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝐿(2 · 𝑦)) = (𝑥𝑀((2 · 𝑦) − 1))) |
50 | | retopon 22377 |
. . . . . . . 8
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
51 | | iccssre 12126 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
52 | 14, 13, 51 | mp2an 704 |
. . . . . . . 8
⊢ (0[,](1 /
2)) ⊆ ℝ |
53 | | resttopon 20775 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
54 | 50, 52, 53 | mp2an 704 |
. . . . . . 7
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
55 | 54 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
56 | 55, 1 | cnmpt2nd 21282 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn 𝐽)) |
57 | 55, 1 | cnmpt1st 21281 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn ((topGen‘ran (,))
↾t (0[,](1 / 2))))) |
58 | 8 | iihalf1cn 22539 |
. . . . . . . 8
⊢ (𝑧 ∈ (0[,](1 / 2)) ↦ (2
· 𝑧)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑧)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
60 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (2 · 𝑧) = (2 · 𝑦)) |
61 | 55, 1, 57, 55, 59, 60 | cnmpt21 21284 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn II)) |
62 | 1, 2, 23 | htpycn 22580 |
. . . . . . 7
⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾)) |
63 | 62, 24 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ((𝐽 ×t II) Cn 𝐾)) |
64 | 55, 1, 56, 61, 63 | cnmpt22f 21288 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ (𝑥𝐿(2 · 𝑦))) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn 𝐾)) |
65 | | iccssre 12126 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
66 | 13, 17, 65 | mp2an 704 |
. . . . . . . 8
⊢ ((1 /
2)[,]1) ⊆ ℝ |
67 | | resttopon 20775 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
68 | 50, 66, 67 | mp2an 704 |
. . . . . . 7
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
69 | 68 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
70 | 69, 1 | cnmpt2nd 21282 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑥 ∈ 𝑋 ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t 𝐽) Cn 𝐽)) |
71 | 69, 1 | cnmpt1st 21281 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑥 ∈ 𝑋 ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t 𝐽) Cn ((topGen‘ran (,))
↾t ((1 / 2)[,]1)))) |
72 | 9 | iihalf2cn 22541 |
. . . . . . . 8
⊢ (𝑧 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑧) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) |
73 | 72 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑧) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
74 | 60 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((2 · 𝑧) − 1) = ((2 · 𝑦) − 1)) |
75 | 69, 1, 71, 69, 73, 74 | cnmpt21 21284 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑥 ∈ 𝑋 ↦ ((2 · 𝑦) − 1)) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t 𝐽) Cn II)) |
76 | 1, 23, 3 | htpycn 22580 |
. . . . . . 7
⊢ (𝜑 → (𝐺(𝐽 Htpy 𝐾)𝐻) ⊆ ((𝐽 ×t II) Cn 𝐾)) |
77 | 76, 27 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ((𝐽 ×t II) Cn 𝐾)) |
78 | 69, 1, 70, 75, 77 | cnmpt22f 21288 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑥 ∈ 𝑋 ↦ (𝑥𝑀((2 · 𝑦) − 1))) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t 𝐽) Cn 𝐾)) |
79 | 7, 8, 9, 10, 11, 12, 22, 1, 49, 64, 78 | cnmpt2pc 22535 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑥 ∈ 𝑋 ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1)))) ∈ ((II
×t 𝐽) Cn
𝐾)) |
80 | 6, 1, 79 | cnmptcom 21291 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1)))) ∈ ((𝐽 ×t II) Cn 𝐾)) |
81 | 4, 80 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝐽 ×t II) Cn 𝐾)) |
82 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → 𝑠 ∈ 𝑋) |
83 | | 0elunit 12161 |
. . . 4
⊢ 0 ∈
(0[,]1) |
84 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 = 0) |
85 | 84, 16 | syl6eqbr 4622 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 ≤ (1 / 2)) |
86 | 85 | iftrued 4044 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑥𝐿(2 · 𝑦))) |
87 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑥 = 𝑠) |
88 | 84 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (2 · 𝑦) = (2 · 0)) |
89 | | 2t0e0 11060 |
. . . . . . . 8
⊢ (2
· 0) = 0 |
90 | 88, 89 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (2 · 𝑦) = 0) |
91 | 87, 90 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝑥𝐿(2 · 𝑦)) = (𝑠𝐿0)) |
92 | 86, 91 | eqtrd 2644 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑠𝐿0)) |
93 | | ovex 6577 |
. . . . 5
⊢ (𝑠𝐿0) ∈ V |
94 | 92, 4, 93 | ovmpt2a 6689 |
. . . 4
⊢ ((𝑠 ∈ 𝑋 ∧ 0 ∈ (0[,]1)) → (𝑠𝑁0) = (𝑠𝐿0)) |
95 | 82, 83, 94 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁0) = (𝑠𝐿0)) |
96 | 25 | simpld 474 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐿0) = (𝐹‘𝑠)) |
97 | 95, 96 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁0) = (𝐹‘𝑠)) |
98 | | 1elunit 12162 |
. . . 4
⊢ 1 ∈
(0[,]1) |
99 | 13, 17 | ltnlei 10037 |
. . . . . . . . 9
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
100 | 18, 99 | mpbi 219 |
. . . . . . . 8
⊢ ¬ 1
≤ (1 / 2) |
101 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑦 = 1) |
102 | 101 | breq1d 4593 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑦 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
103 | 100, 102 | mtbiri 316 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ¬ 𝑦 ≤ (1 / 2)) |
104 | 103 | iffalsed 4047 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑥𝑀((2 · 𝑦) − 1))) |
105 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑥 = 𝑠) |
106 | 101 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (2 · 𝑦) = (2 · 1)) |
107 | | 2t1e2 11053 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
108 | 106, 107 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (2 · 𝑦) = 2) |
109 | 108 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑦) − 1) = (2 −
1)) |
110 | | 2m1e1 11012 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
111 | 109, 110 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑦) − 1) = 1) |
112 | 105, 111 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑥𝑀((2 · 𝑦) − 1)) = (𝑠𝑀1)) |
113 | 104, 112 | eqtrd 2644 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑠𝑀1)) |
114 | | ovex 6577 |
. . . . 5
⊢ (𝑠𝑀1) ∈ V |
115 | 113, 4, 114 | ovmpt2a 6689 |
. . . 4
⊢ ((𝑠 ∈ 𝑋 ∧ 1 ∈ (0[,]1)) → (𝑠𝑁1) = (𝑠𝑀1)) |
116 | 82, 98, 115 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁1) = (𝑠𝑀1)) |
117 | 28 | simprd 478 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑀1) = (𝐻‘𝑠)) |
118 | 116, 117 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁1) = (𝐻‘𝑠)) |
119 | 1, 2, 3, 81, 97, 118 | ishtpyd 22582 |
1
⊢ (𝜑 → 𝑁 ∈ (𝐹(𝐽 Htpy 𝐾)𝐻)) |