Detailed syntax breakdown of Definition df-leop
Step | Hyp | Ref
| Expression |
1 | | cleo 27815 |
. 2
class
≤op |
2 | | vu |
. . . . . . 7
setvar 𝑢 |
3 | 2 | cv 1482 |
. . . . . 6
class 𝑢 |
4 | | vt |
. . . . . . 7
setvar 𝑡 |
5 | 4 | cv 1482 |
. . . . . 6
class 𝑡 |
6 | | chod 27797 |
. . . . . 6
class
−op |
7 | 3, 5, 6 | co 6650 |
. . . . 5
class (𝑢 −op 𝑡) |
8 | | cho 27807 |
. . . . 5
class
HrmOp |
9 | 7, 8 | wcel 1990 |
. . . 4
wff (𝑢 −op 𝑡) ∈ HrmOp |
10 | | cc0 9936 |
. . . . . 6
class
0 |
11 | | vx |
. . . . . . . . 9
setvar 𝑥 |
12 | 11 | cv 1482 |
. . . . . . . 8
class 𝑥 |
13 | 12, 7 | cfv 5888 |
. . . . . . 7
class ((𝑢 −op 𝑡)‘𝑥) |
14 | | csp 27779 |
. . . . . . 7
class
·ih |
15 | 13, 12, 14 | co 6650 |
. . . . . 6
class (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥) |
16 | | cle 10075 |
. . . . . 6
class
≤ |
17 | 10, 15, 16 | wbr 4653 |
. . . . 5
wff 0 ≤
(((𝑢 −op
𝑡)‘𝑥) ·ih 𝑥) |
18 | | chil 27776 |
. . . . 5
class
ℋ |
19 | 17, 11, 18 | wral 2912 |
. . . 4
wff
∀𝑥 ∈
ℋ 0 ≤ (((𝑢
−op 𝑡)‘𝑥) ·ih 𝑥) |
20 | 9, 19 | wa 384 |
. . 3
wff ((𝑢 −op 𝑡) ∈ HrmOp ∧
∀𝑥 ∈ ℋ 0
≤ (((𝑢
−op 𝑡)‘𝑥) ·ih 𝑥)) |
21 | 20, 4, 2 | copab 4712 |
. 2
class
{〈𝑡, 𝑢〉 ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧
∀𝑥 ∈ ℋ 0
≤ (((𝑢
−op 𝑡)‘𝑥) ·ih 𝑥))} |
22 | 1, 21 | wceq 1483 |
1
wff
≤op = {〈𝑡, 𝑢〉 ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))} |