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		ffvelcdm	⊢ ( ( 𝐹 : ( 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	eqtrid	⊢ ( ( ( 𝐹 ∈ ( 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 ‘ 𝐽 ) 𝐹 )