Step |
Hyp |
Ref |
Expression |
0 |
|
cpco |
⊢ *𝑝 |
1 |
|
vj |
⊢ 𝑗 |
2 |
|
ctop |
⊢ Top |
3 |
|
vf |
⊢ 𝑓 |
4 |
|
cii |
⊢ II |
5 |
|
ccn |
⊢ Cn |
6 |
1
|
cv |
⊢ 𝑗 |
7 |
4 6 5
|
co |
⊢ ( II Cn 𝑗 ) |
8 |
|
vg |
⊢ 𝑔 |
9 |
|
vx |
⊢ 𝑥 |
10 |
|
cc0 |
⊢ 0 |
11 |
|
cicc |
⊢ [,] |
12 |
|
c1 |
⊢ 1 |
13 |
10 12 11
|
co |
⊢ ( 0 [,] 1 ) |
14 |
9
|
cv |
⊢ 𝑥 |
15 |
|
cle |
⊢ ≤ |
16 |
|
cdiv |
⊢ / |
17 |
|
c2 |
⊢ 2 |
18 |
12 17 16
|
co |
⊢ ( 1 / 2 ) |
19 |
14 18 15
|
wbr |
⊢ 𝑥 ≤ ( 1 / 2 ) |
20 |
3
|
cv |
⊢ 𝑓 |
21 |
|
cmul |
⊢ · |
22 |
17 14 21
|
co |
⊢ ( 2 · 𝑥 ) |
23 |
22 20
|
cfv |
⊢ ( 𝑓 ‘ ( 2 · 𝑥 ) ) |
24 |
8
|
cv |
⊢ 𝑔 |
25 |
|
cmin |
⊢ − |
26 |
22 12 25
|
co |
⊢ ( ( 2 · 𝑥 ) − 1 ) |
27 |
26 24
|
cfv |
⊢ ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) |
28 |
19 23 27
|
cif |
⊢ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) |
29 |
9 13 28
|
cmpt |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) |
30 |
3 8 7 7 29
|
cmpo |
⊢ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) |
31 |
1 2 30
|
cmpt |
⊢ ( 𝑗 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) ) |
32 |
0 31
|
wceq |
⊢ *𝑝 = ( 𝑗 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) ) |