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 22682 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
6 | 5 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
7 | | eqid 2622 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
8 | | eqid 2622 |
. . . . 5
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
9 | | eqid 2622 |
. . . . 5
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
10 | | dfii2 22685 |
. . . . 5
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
11 | | 0red 10041 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ) |
12 | | 1red 10055 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
13 | | halfre 11246 |
. . . . . . 7
⊢ (1 / 2)
∈ ℝ |
14 | | 0re 10040 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
15 | | halfgt0 11248 |
. . . . . . . 8
⊢ 0 < (1
/ 2) |
16 | 14, 13, 15 | ltleii 10160 |
. . . . . . 7
⊢ 0 ≤ (1
/ 2) |
17 | | 1re 10039 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
18 | | halflt1 11250 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
19 | 13, 17, 18 | ltleii 10160 |
. . . . . . 7
⊢ (1 / 2)
≤ 1 |
20 | 14, 17 | elicc2i 12239 |
. . . . . . 7
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
21 | 13, 16, 19, 20 | mpbir3an 1244 |
. . . . . 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 22773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝑠𝐿0) = (𝐹‘𝑠) ∧ (𝑠𝐿1) = (𝐺‘𝑠))) |
26 | 25 | simprd 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐿1) = (𝐺‘𝑠)) |
27 | | htpycc.8 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (𝐺(𝐽 Htpy 𝐾)𝐻)) |
28 | 1, 23, 3, 27 | htpyi 22773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → ((𝑠𝑀0) = (𝐺‘𝑠) ∧ (𝑠𝑀1) = (𝐻‘𝑠))) |
29 | 28 | simpld 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑀0) = (𝐺‘𝑠)) |
30 | 26, 29 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐿1) = (𝑠𝑀0)) |
31 | 30 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑠 ∈ 𝑋 (𝑠𝐿1) = (𝑠𝑀0)) |
32 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → (𝑠𝐿1) = (𝑥𝐿1)) |
33 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → (𝑠𝑀0) = (𝑥𝑀0)) |
34 | 32, 33 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑠 = 𝑥 → ((𝑠𝐿1) = (𝑠𝑀0) ↔ (𝑥𝐿1) = (𝑥𝑀0))) |
35 | 34 | rspccva 3308 |
. . . . . . . 8
⊢
((∀𝑠 ∈
𝑋 (𝑠𝐿1) = (𝑠𝑀0) ∧ 𝑥 ∈ 𝑋) → (𝑥𝐿1) = (𝑥𝑀0)) |
36 | 31, 35 | sylan 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐿1) = (𝑥𝑀0)) |
37 | 36 | adantrl 752 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝐿1) = (𝑥𝑀0)) |
38 | | simprl 794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → 𝑦 = (1 / 2)) |
39 | 38 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (2 · 𝑦) = (2 · (1 / 2))) |
40 | | 2cn 11091 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
41 | | 2ne0 11113 |
. . . . . . . . 9
⊢ 2 ≠
0 |
42 | 40, 41 | recidi 10756 |
. . . . . . . 8
⊢ (2
· (1 / 2)) = 1 |
43 | 39, 42 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (2 · 𝑦) = 1) |
44 | 43 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝐿(2 · 𝑦)) = (𝑥𝐿1)) |
45 | 43 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → ((2 · 𝑦) − 1) = (1 −
1)) |
46 | | 1m1e0 11089 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
47 | 45, 46 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → ((2 · 𝑦) − 1) = 0) |
48 | 47 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝑀((2 · 𝑦) − 1)) = (𝑥𝑀0)) |
49 | 37, 44, 48 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑥 ∈ 𝑋)) → (𝑥𝐿(2 · 𝑦)) = (𝑥𝑀((2 · 𝑦) − 1))) |
50 | | retopon 22567 |
. . . . . . . 8
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
51 | | iccssre 12255 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
52 | 14, 13, 51 | mp2an 708 |
. . . . . . . 8
⊢ (0[,](1 /
2)) ⊆ ℝ |
53 | | resttopon 20965 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
54 | 50, 52, 53 | mp2an 708 |
. . . . . . 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 21472 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn 𝐽)) |
57 | 55, 1 | cnmpt1st 21471 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn ((topGen‘ran (,))
↾t (0[,](1 / 2))))) |
58 | 8 | iihalf1cn 22731 |
. . . . . . . 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 6658 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (2 · 𝑧) = (2 · 𝑦)) |
61 | 55, 1, 57, 55, 59, 60 | cnmpt21 21474 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn II)) |
62 | 1, 2, 23 | htpycn 22772 |
. . . . . . 7
⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾)) |
63 | 62, 24 | sseldd 3604 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ((𝐽 ×t II) Cn 𝐾)) |
64 | 55, 1, 56, 61, 63 | cnmpt22f 21478 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑥 ∈ 𝑋 ↦ (𝑥𝐿(2 · 𝑦))) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t 𝐽) Cn 𝐾)) |
65 | | iccssre 12255 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
66 | 13, 17, 65 | mp2an 708 |
. . . . . . . 8
⊢ ((1 /
2)[,]1) ⊆ ℝ |
67 | | resttopon 20965 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
68 | 50, 66, 67 | mp2an 708 |
. . . . . . 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 21472 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑥 ∈ 𝑋 ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t 𝐽) Cn 𝐽)) |
71 | 69, 1 | cnmpt1st 21471 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑥 ∈ 𝑋 ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t 𝐽) Cn ((topGen‘ran (,))
↾t ((1 / 2)[,]1)))) |
72 | 9 | iihalf2cn 22733 |
. . . . . . . 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 6665 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((2 · 𝑧) − 1) = ((2 · 𝑦) − 1)) |
75 | 69, 1, 71, 69, 73, 74 | cnmpt21 21474 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑥 ∈ 𝑋 ↦ ((2 · 𝑦) − 1)) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t 𝐽) Cn II)) |
76 | 1, 23, 3 | htpycn 22772 |
. . . . . . 7
⊢ (𝜑 → (𝐺(𝐽 Htpy 𝐾)𝐻) ⊆ ((𝐽 ×t II) Cn 𝐾)) |
77 | 76, 27 | sseldd 3604 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ((𝐽 ×t II) Cn 𝐾)) |
78 | 69, 1, 70, 75, 77 | cnmpt22f 21478 |
. . . . 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 22727 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑥 ∈ 𝑋 ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1)))) ∈ ((II
×t 𝐽) Cn
𝐾)) |
80 | 6, 1, 79 | cnmptcom 21481 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1)))) ∈ ((𝐽 ×t II) Cn 𝐾)) |
81 | 4, 80 | syl5eqel 2705 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝐽 ×t II) Cn 𝐾)) |
82 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → 𝑠 ∈ 𝑋) |
83 | | 0elunit 12290 |
. . . 4
⊢ 0 ∈
(0[,]1) |
84 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 = 0) |
85 | 84, 16 | syl6eqbr 4692 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 ≤ (1 / 2)) |
86 | 85 | iftrued 4094 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑥𝐿(2 · 𝑦))) |
87 | | simpl 473 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑥 = 𝑠) |
88 | 84 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (2 · 𝑦) = (2 · 0)) |
89 | | 2t0e0 11183 |
. . . . . . . 8
⊢ (2
· 0) = 0 |
90 | 88, 89 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (2 · 𝑦) = 0) |
91 | 87, 90 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝑥𝐿(2 · 𝑦)) = (𝑠𝐿0)) |
92 | 86, 91 | eqtrd 2656 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑠𝐿0)) |
93 | | ovex 6678 |
. . . . 5
⊢ (𝑠𝐿0) ∈ V |
94 | 92, 4, 93 | ovmpt2a 6791 |
. . . 4
⊢ ((𝑠 ∈ 𝑋 ∧ 0 ∈ (0[,]1)) → (𝑠𝑁0) = (𝑠𝐿0)) |
95 | 82, 83, 94 | sylancl 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁0) = (𝑠𝐿0)) |
96 | 25 | simpld 475 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐿0) = (𝐹‘𝑠)) |
97 | 95, 96 | eqtrd 2656 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁0) = (𝐹‘𝑠)) |
98 | | 1elunit 12291 |
. . . 4
⊢ 1 ∈
(0[,]1) |
99 | 13, 17 | ltnlei 10158 |
. . . . . . . . 9
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
100 | 18, 99 | mpbi 220 |
. . . . . . . 8
⊢ ¬ 1
≤ (1 / 2) |
101 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑦 = 1) |
102 | 101 | breq1d 4663 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑦 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
103 | 100, 102 | mtbiri 317 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ¬ 𝑦 ≤ (1 / 2)) |
104 | 103 | iffalsed 4097 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑥𝑀((2 · 𝑦) − 1))) |
105 | | simpl 473 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑥 = 𝑠) |
106 | 101 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (2 · 𝑦) = (2 · 1)) |
107 | | 2t1e2 11176 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
108 | 106, 107 | syl6eq 2672 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (2 · 𝑦) = 2) |
109 | 108 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑦) − 1) = (2 −
1)) |
110 | | 2m1e1 11135 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
111 | 109, 110 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑦) − 1) = 1) |
112 | 105, 111 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑥𝑀((2 · 𝑦) − 1)) = (𝑠𝑀1)) |
113 | 104, 112 | eqtrd 2656 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))) = (𝑠𝑀1)) |
114 | | ovex 6678 |
. . . . 5
⊢ (𝑠𝑀1) ∈ V |
115 | 113, 4, 114 | ovmpt2a 6791 |
. . . 4
⊢ ((𝑠 ∈ 𝑋 ∧ 1 ∈ (0[,]1)) → (𝑠𝑁1) = (𝑠𝑀1)) |
116 | 82, 98, 115 | sylancl 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁1) = (𝑠𝑀1)) |
117 | 28 | simprd 479 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑀1) = (𝐻‘𝑠)) |
118 | 116, 117 | eqtrd 2656 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝑁1) = (𝐻‘𝑠)) |
119 | 1, 2, 3, 81, 97, 118 | ishtpyd 22774 |
1
⊢ (𝜑 → 𝑁 ∈ (𝐹(𝐽 Htpy 𝐾)𝐻)) |