Metamath Proof Explorer


Theorem pcopt2

Description: Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015)

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

Proof

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