Metamath Proof Explorer

Theorem htpycc

Description: Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses htpycc.1 ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) )
htpycc.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
htpycc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
htpycc.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
htpycc.6 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐽 Cn 𝐾 ) )
htpycc.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
htpycc.8 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )
Assertion htpycc ( 𝜑 → 𝑁 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )

Proof

Step Hyp Ref Expression
1 htpycc.1 ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) )
2 htpycc.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 htpycc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 htpycc.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
5 htpycc.6 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐽 Cn 𝐾 ) )
6 htpycc.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
7 htpycc.8 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )
8 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
9 8 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
10 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
11 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
12 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
13 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
14 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
15 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
16 halfre ⊢ ( 1 / 2 ) ∈ ℝ
17 halfge0 ⊢ 0 ≤ ( 1 / 2 )
18 1re ⊢ 1 ∈ ℝ
19 halflt1 ⊢ ( 1 / 2 ) < 1
20 16 18 19 ltleii ⊢ ( 1 / 2 ) ≤ 1
21 elicc01 ⊢ ( ( 1 / 2 ) ∈ ( 0 [,] 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 1 ) )
22 16 17 20 21 mpbir3an ⊢ ( 1 / 2 ) ∈ ( 0 [,] 1 )
23 22 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ( 0 [,] 1 ) )
24 2 3 4 6 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑠 𝐿 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐿 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
25 24 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐿 1 ) = ( 𝐺 ‘ 𝑠 ) )
26 2 4 5 7 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑠 𝑀 0 ) = ( 𝐺 ‘ 𝑠 ) ∧ ( 𝑠 𝑀 1 ) = ( 𝐻 ‘ 𝑠 ) ) )
27 26 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑀 0 ) = ( 𝐺 ‘ 𝑠 ) )
28 25 27 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑋 ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) )
30 oveq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 𝐿 1 ) = ( 𝑥 𝐿 1 ) )
31 oveq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 𝑀 0 ) = ( 𝑥 𝑀 0 ) )
32 30 31 eqeq12d ⊢ ( 𝑠 = 𝑥 → ( ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) ↔ ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) ) )
33 32 rspccva ⊢ ( ( ∀ 𝑠 ∈ 𝑋 ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) )
34 29 33 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) )
35 34 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) )
36 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → 𝑦 = ( 1 / 2 ) )
37 36 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 2 · 𝑦 ) = ( 2 · ( 1 / 2 ) ) )
38 2thalfe1 ⊢ ( 2 · ( 1 / 2 ) ) = 1
39 37 38 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 2 · 𝑦 ) = 1 )
40 39 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝐿 ( 2 · 𝑦 ) ) = ( 𝑥 𝐿 1 ) )
41 39 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 2 · 𝑦 ) − 1 ) = ( 1 − 1 ) )
42 1m1e0 ⊢ ( 1 − 1 ) = 0
43 41 42 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 2 · 𝑦 ) − 1 ) = 0 )
44 43 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝑥 𝑀 0 ) )
45 35 40 44 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝐿 ( 2 · 𝑦 ) ) = ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) )
46 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
47 0re ⊢ 0 ∈ ℝ
48 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
49 47 16 48 mp2an ⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
50 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
51 46 49 50 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) )
52 51 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
53 52 2 cnmpt2nd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn 𝐽 ) )
54 52 2 cnmpt1st ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ) )
55 11 iihalf1cn ⊢ ( 𝑧 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑧 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
56 55 a1i ⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑧 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
57 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 2 · 𝑧 ) = ( 2 · 𝑦 ) )
58 52 2 54 52 56 57 cnmpt21 ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ ( 2 · 𝑦 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn II ) )
59 2 3 4 htpycn ⊢ ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
60 59 6 sseldd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
61 52 2 53 58 60 cnmpt22f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐿 ( 2 · 𝑦 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn 𝐾 ) )
62 iccssre ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
63 16 18 62 mp2an ⊢ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
64 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
65 46 63 64 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) )
66 65 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
67 66 2 cnmpt2nd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn 𝐽 ) )
68 66 2 cnmpt1st ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
69 12 iihalf2cn ⊢ ( 𝑧 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑧 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
70 69 a1i ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑧 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
71 57 oveq1d ⊢ ( 𝑧 = 𝑦 → ( ( 2 · 𝑧 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
72 66 2 68 66 70 71 cnmpt21 ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn II ) )
73 2 4 5 htpycn ⊢ ( 𝜑 → ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐻 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
74 73 7 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
75 66 2 67 72 74 cnmpt22f ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn 𝐾 ) )
76 10 11 12 13 14 15 23 2 45 61 75 cnmpopc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑥 ∈ 𝑋 ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) ) ∈ ( ( II ×t 𝐽 ) Cn 𝐾 ) )
77 9 2 76 cnmptcom ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) ) ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
78 1 77 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
79 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝑠 ∈ 𝑋 )
80 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
81 simpr ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑦 = 0 )
82 81 17 eqbrtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑦 ≤ ( 1 / 2 ) )
83 82 iftrued ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑥 𝐿 ( 2 · 𝑦 ) ) )
84 simpl ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑥 = 𝑠 )
85 81 oveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 2 · 𝑦 ) = ( 2 · 0 ) )
86 2t0e0 ⊢ ( 2 · 0 ) = 0
87 85 86 eqtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 2 · 𝑦 ) = 0 )
88 84 87 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 𝑥 𝐿 ( 2 · 𝑦 ) ) = ( 𝑠 𝐿 0 ) )
89 83 88 eqtrd ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑠 𝐿 0 ) )
90 ovex ⊢ ( 𝑠 𝐿 0 ) ∈ V
91 89 1 90 ovmpoa ⊢ ( ( 𝑠 ∈ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑁 0 ) = ( 𝑠 𝐿 0 ) )
92 79 80 91 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 0 ) = ( 𝑠 𝐿 0 ) )
93 24 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐿 0 ) = ( 𝐹 ‘ 𝑠 ) )
94 92 93 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 0 ) = ( 𝐹 ‘ 𝑠 ) )
95 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
96 16 18 ltnlei ⊢ ( ( 1 / 2 ) < 1 ↔ ¬ 1 ≤ ( 1 / 2 ) )
97 19 96 mpbi ⊢ ¬ 1 ≤ ( 1 / 2 )
98 simpr ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → 𝑦 = 1 )
99 98 breq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 𝑦 ≤ ( 1 / 2 ) ↔ 1 ≤ ( 1 / 2 ) ) )
100 97 99 mtbiri ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ¬ 𝑦 ≤ ( 1 / 2 ) )
101 100 iffalsed ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) )
102 simpl ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → 𝑥 = 𝑠 )
103 98 oveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 2 · 𝑦 ) = ( 2 · 1 ) )
104 2t1e2 ⊢ ( 2 · 1 ) = 2
105 103 104 eqtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 2 · 𝑦 ) = 2 )
106 105 oveq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( 2 · 𝑦 ) − 1 ) = ( 2 − 1 ) )
107 2m1e1 ⊢ ( 2 − 1 ) = 1
108 106 107 eqtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( 2 · 𝑦 ) − 1 ) = 1 )
109 102 108 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝑠 𝑀 1 ) )
110 101 109 eqtrd ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑠 𝑀 1 ) )
111 ovex ⊢ ( 𝑠 𝑀 1 ) ∈ V
112 110 1 111 ovmpoa ⊢ ( ( 𝑠 ∈ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑁 1 ) = ( 𝑠 𝑀 1 ) )
113 79 95 112 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 1 ) = ( 𝑠 𝑀 1 ) )
114 26 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑀 1 ) = ( 𝐻 ‘ 𝑠 ) )
115 113 114 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 1 ) = ( 𝐻 ‘ 𝑠 ) )
116 2 3 5 78 94 115 ishtpyd ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )