Metamath Proof Explorer

Theorem pcopt

Description: Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

Ref Expression
Hypothesis pcopt.1 ⊢ 𝑃 = ( ( 0 [,] 1 ) × { 𝑌 } )
Assertion pcopt ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( ≃ph ‘ 𝐽 ) 𝐹 )

Proof

Step Hyp Ref Expression
1 pcopt.1 ⊢ 𝑃 = ( ( 0 [,] 1 ) × { 𝑌 } )
2 1 fveq1i ⊢ ( 𝑃 ‘ ( 2 · 𝑥 ) ) = ( ( ( 0 [,] 1 ) × { 𝑌 } ) ‘ ( 2 · 𝑥 ) )
3 simpr ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝐹 ‘ 0 ) = 𝑌 )
4 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
5 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
6 4 5 cnf ⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐹 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
7 6 adantr ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 𝐹 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
8 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
9 ffvelrn ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 0 ) ∈ ∪ 𝐽 )
10 7 8 9 sylancl ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝐹 ‘ 0 ) ∈ ∪ 𝐽 )
11 3 10 eqeltrrd ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 𝑌 ∈ ∪ 𝐽 )
12 elii1 ⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) )
13 iihalf1 ⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
14 12 13 sylbir ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
15 fvconst2g ⊢ ( ( 𝑌 ∈ ∪ 𝐽 ∧ ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { 𝑌 } ) ‘ ( 2 · 𝑥 ) ) = 𝑌 )
16 11 14 15 syl2an ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ) → ( ( ( 0 [,] 1 ) × { 𝑌 } ) ‘ ( 2 · 𝑥 ) ) = 𝑌 )
17 2 16 syl5eq ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ) → ( 𝑃 ‘ ( 2 · 𝑥 ) ) = 𝑌 )
18 simplr ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ) → ( 𝐹 ‘ 0 ) = 𝑌 )
19 17 18 eqtr4d ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ) → ( 𝑃 ‘ ( 2 · 𝑥 ) ) = ( 𝐹 ‘ 0 ) )
20 19 ifeq1d ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑃 ‘ ( 2 · 𝑥 ) ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
21 20 expr ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑃 ‘ ( 2 · 𝑥 ) ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
22 iffalse ⊢ ( ¬ 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑃 ‘ ( 2 · 𝑥 ) ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
23 iffalse ⊢ ( ¬ 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
24 22 23 eqtr4d ⊢ ( ¬ 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑃 ‘ ( 2 · 𝑥 ) ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
25 21 24 pm2.61d1 ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑃 ‘ ( 2 · 𝑥 ) ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
26 25 mpteq2dva ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑃 ‘ ( 2 · 𝑥 ) ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
27 cntop2 ⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐽 ∈ Top )
28 27 adantr ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 𝐽 ∈ Top )
29 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
30 28 29 sylib ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
31 1 pcoptcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝑌 ∈ ∪ 𝐽 ) → ( 𝑃 ∈ ( II Cn 𝐽 ) ∧ ( 𝑃 ‘ 0 ) = 𝑌 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) )
32 30 11 31 syl2anc ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑃 ∈ ( II Cn 𝐽 ) ∧ ( 𝑃 ‘ 0 ) = 𝑌 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) )
33 32 simp1d ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 𝑃 ∈ ( II Cn 𝐽 ) )
34 simpl ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 𝐹 ∈ ( II Cn 𝐽 ) )
35 33 34 pcoval ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐹 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑃 ‘ ( 2 · 𝑥 ) ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
36 iffalse ⊢ ( ¬ 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) = ( ( 2 · 𝑥 ) − 1 ) )
37 36 adantl ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) = ( ( 2 · 𝑥 ) − 1 ) )
38 elii2 ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) )
39 iihalf2 ⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) )
40 38 39 syl ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) )
41 37 40 eqeltrd ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 0 [,] 1 ) )
42 41 ex ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 0 [,] 1 ) ) )
43 iftrue ⊢ ( 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) = 0 )
44 43 8 eqeltrdi ⊢ ( 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 0 [,] 1 ) )
45 42 44 pm2.61d2 ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 0 [,] 1 ) )
46 45 adantl ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 0 [,] 1 ) )
47 eqid ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) )
48 47 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) )
49 7 feqmptd ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 𝐹 = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
50 fveq2 ⊢ ( 𝑦 = if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) )
51 fvif ⊢ ( 𝐹 ‘ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
52 50 51 eqtrdi ⊢ ( 𝑦 = if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
53 46 48 49 52 fmptco ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝐹 ∘ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
54 26 35 53 3eqtr4d ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐹 ) = ( 𝐹 ∘ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
55 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
56 55 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
57 56 cnmptid ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( II Cn II ) )
58 8 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 0 ∈ ( 0 [,] 1 ) )
59 56 56 58 cnmptc ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 0 ) ∈ ( II Cn II ) )
60 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
61 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
62 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
63 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
64 0re ⊢ 0 ∈ ℝ
65 64 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 0 ∈ ℝ )
66 1re ⊢ 1 ∈ ℝ
67 66 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → 1 ∈ ℝ )
68 halfre ⊢ ( 1 / 2 ) ∈ ℝ
69 halfge0 ⊢ 0 ≤ ( 1 / 2 )
70 halflt1 ⊢ ( 1 / 2 ) < 1
71 68 66 70 ltleii ⊢ ( 1 / 2 ) ≤ 1
72 elicc01 ⊢ ( ( 1 / 2 ) ∈ ( 0 [,] 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 1 ) )
73 68 69 71 72 mpbir3an ⊢ ( 1 / 2 ) ∈ ( 0 [,] 1 )
74 73 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 1 / 2 ) ∈ ( 0 [,] 1 ) )
75 simprl ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → 𝑦 = ( 1 / 2 ) )
76 75 oveq2d ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑦 ) = ( 2 · ( 1 / 2 ) ) )
77 2cn ⊢ 2 ∈ ℂ
78 2ne0 ⊢ 2 ≠ 0
79 77 78 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
80 76 79 eqtrdi ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑦 ) = 1 )
81 80 oveq1d ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑦 ) − 1 ) = ( 1 − 1 ) )
82 1m1e0 ⊢ ( 1 − 1 ) = 0
83 81 82 eqtr2di ⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → 0 = ( ( 2 · 𝑦 ) − 1 ) )
84 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
85 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
86 64 68 85 mp2an ⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
87 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
88 84 86 87 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) )
89 88 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
90 89 56 56 58 cnmpt2c ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 0 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn II ) )
91 iccssre ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
92 68 66 91 mp2an ⊢ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
93 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
94 84 92 93 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) )
95 94 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
96 95 56 cnmpt1st ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
97 62 iihalf2cn ⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
98 97 a1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
99 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
100 99 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
101 95 56 96 95 98 100 cnmpt21 ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn II ) )
102 60 61 62 63 65 67 74 56 83 90 101 cnmpopc ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑦 ) − 1 ) ) ) ∈ ( ( II ×t II ) Cn II ) )
103 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 1 / 2 ) ↔ 𝑥 ≤ ( 1 / 2 ) ) )
104 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) )
105 104 oveq1d ⊢ ( 𝑦 = 𝑥 → ( ( 2 · 𝑦 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
106 103 105 ifbieq2d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑦 ) − 1 ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) )
107 106 adantr ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑧 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑦 ) − 1 ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) )
108 56 57 59 56 56 102 107 cnmpt12 ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ∈ ( II Cn II ) )
109 id ⊢ ( 𝑥 = 0 → 𝑥 = 0 )
110 109 69 eqbrtrdi ⊢ ( 𝑥 = 0 → 𝑥 ≤ ( 1 / 2 ) )
111 110 43 syl ⊢ ( 𝑥 = 0 → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) = 0 )
112 c0ex ⊢ 0 ∈ V
113 111 47 112 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ‘ 0 ) = 0 )
114 8 113 mp1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ‘ 0 ) = 0 )
115 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
116 68 66 ltnlei ⊢ ( ( 1 / 2 ) < 1 ↔ ¬ 1 ≤ ( 1 / 2 ) )
117 70 116 mpbi ⊢ ¬ 1 ≤ ( 1 / 2 )
118 breq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ≤ ( 1 / 2 ) ↔ 1 ≤ ( 1 / 2 ) ) )
119 117 118 mtbiri ⊢ ( 𝑥 = 1 → ¬ 𝑥 ≤ ( 1 / 2 ) )
120 119 36 syl ⊢ ( 𝑥 = 1 → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) = ( ( 2 · 𝑥 ) − 1 ) )
121 oveq2 ⊢ ( 𝑥 = 1 → ( 2 · 𝑥 ) = ( 2 · 1 ) )
122 2t1e2 ⊢ ( 2 · 1 ) = 2
123 121 122 eqtrdi ⊢ ( 𝑥 = 1 → ( 2 · 𝑥 ) = 2 )
124 123 oveq1d ⊢ ( 𝑥 = 1 → ( ( 2 · 𝑥 ) − 1 ) = ( 2 − 1 ) )
125 2m1e1 ⊢ ( 2 − 1 ) = 1
126 124 125 eqtrdi ⊢ ( 𝑥 = 1 → ( ( 2 · 𝑥 ) − 1 ) = 1 )
127 120 126 eqtrd ⊢ ( 𝑥 = 1 → if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) = 1 )
128 1ex ⊢ 1 ∈ V
129 127 47 128 fvmpt ⊢ ( 1 ∈ ( 0 [,] 1 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ‘ 1 ) = 1 )
130 115 129 mp1i ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ‘ 1 ) = 1 )
131 34 108 114 130 reparpht ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝐹 ∘ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , 0 , ( ( 2 · 𝑥 ) − 1 ) ) ) ) ( ≃ph ‘ 𝐽 ) 𝐹 )
132 54 131 eqbrtrd ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) → ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( ≃ph ‘ 𝐽 ) 𝐹 )