Detailed syntax breakdown of Definition df-pco
Step | Hyp | Ref
| Expression |
1 | | cpco 24163 |
. 2
class
*𝑝 |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | ctop 22042 |
. . 3
class
Top |
4 | | vf |
. . . 4
setvar 𝑓 |
5 | | vg |
. . . 4
setvar 𝑔 |
6 | | cii 24038 |
. . . . 5
class
II |
7 | 2 | cv 1538 |
. . . . 5
class 𝑗 |
8 | | ccn 22375 |
. . . . 5
class
Cn |
9 | 6, 7, 8 | co 7275 |
. . . 4
class (II Cn
𝑗) |
10 | | vx |
. . . . 5
setvar 𝑥 |
11 | | cc0 10871 |
. . . . . 6
class
0 |
12 | | c1 10872 |
. . . . . 6
class
1 |
13 | | cicc 13082 |
. . . . . 6
class
[,] |
14 | 11, 12, 13 | co 7275 |
. . . . 5
class
(0[,]1) |
15 | 10 | cv 1538 |
. . . . . . 7
class 𝑥 |
16 | | c2 12028 |
. . . . . . . 8
class
2 |
17 | | cdiv 11632 |
. . . . . . . 8
class
/ |
18 | 12, 16, 17 | co 7275 |
. . . . . . 7
class (1 /
2) |
19 | | cle 11010 |
. . . . . . 7
class
≤ |
20 | 15, 18, 19 | wbr 5074 |
. . . . . 6
wff 𝑥 ≤ (1 / 2) |
21 | | cmul 10876 |
. . . . . . . 8
class
· |
22 | 16, 15, 21 | co 7275 |
. . . . . . 7
class (2
· 𝑥) |
23 | 4 | cv 1538 |
. . . . . . 7
class 𝑓 |
24 | 22, 23 | cfv 6433 |
. . . . . 6
class (𝑓‘(2 · 𝑥)) |
25 | | cmin 11205 |
. . . . . . . 8
class
− |
26 | 22, 12, 25 | co 7275 |
. . . . . . 7
class ((2
· 𝑥) −
1) |
27 | 5 | cv 1538 |
. . . . . . 7
class 𝑔 |
28 | 26, 27 | cfv 6433 |
. . . . . 6
class (𝑔‘((2 · 𝑥) − 1)) |
29 | 20, 24, 28 | cif 4459 |
. . . . 5
class if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))) |
30 | 10, 14, 29 | cmpt 5157 |
. . . 4
class (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))) |
31 | 4, 5, 9, 9, 30 | cmpo 7277 |
. . 3
class (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) |
32 | 2, 3, 31 | cmpt 5157 |
. 2
class (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |
33 | 1, 32 | wceq 1539 |
1
wff
*𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |