Detailed syntax breakdown of Definition df-left
Step | Hyp | Ref
| Expression |
1 | | cleft 34038 |
. 2
class
L |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | csur 33852 |
. . 3
class No |
4 | | vy |
. . . . . 6
setvar 𝑦 |
5 | 4 | cv 1538 |
. . . . 5
class 𝑦 |
6 | 2 | cv 1538 |
. . . . 5
class 𝑥 |
7 | | cslt 33853 |
. . . . 5
class
<s |
8 | 5, 6, 7 | wbr 5075 |
. . . 4
wff 𝑦 <s 𝑥 |
9 | | cbday 33854 |
. . . . . 6
class bday |
10 | 6, 9 | cfv 6437 |
. . . . 5
class ( bday ‘𝑥) |
11 | | cold 34036 |
. . . . 5
class
O |
12 | 10, 11 | cfv 6437 |
. . . 4
class ( O
‘( bday ‘𝑥)) |
13 | 8, 4, 12 | crab 3069 |
. . 3
class {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥} |
14 | 2, 3, 13 | cmpt 5158 |
. 2
class (𝑥 ∈
No ↦ {𝑦
∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥}) |
15 | 1, 14 | wceq 1539 |
1
wff L = (𝑥 ∈
No ↦ {𝑦
∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥}) |