Detailed syntax breakdown of Definition df-left
Step | Hyp | Ref
| Expression |
1 | | cleft 31928 |
. 2
class
L |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | csur 31793 |
. . 3
class No |
4 | | vy |
. . . . . . . . 9
setvar 𝑦 |
5 | 4 | cv 1482 |
. . . . . . . 8
class 𝑦 |
6 | | vz |
. . . . . . . . 9
setvar 𝑧 |
7 | 6 | cv 1482 |
. . . . . . . 8
class 𝑧 |
8 | | cslt 31794 |
. . . . . . . 8
class
<s |
9 | 5, 7, 8 | wbr 4653 |
. . . . . . 7
wff 𝑦 <s 𝑧 |
10 | 2 | cv 1482 |
. . . . . . . 8
class 𝑥 |
11 | 7, 10, 8 | wbr 4653 |
. . . . . . 7
wff 𝑧 <s 𝑥 |
12 | 9, 11 | wa 384 |
. . . . . 6
wff (𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) |
13 | | cbday 31795 |
. . . . . . . 8
class bday |
14 | 5, 13 | cfv 5888 |
. . . . . . 7
class ( bday ‘𝑦) |
15 | 7, 13 | cfv 5888 |
. . . . . . 7
class ( bday ‘𝑧) |
16 | 14, 15 | wcel 1990 |
. . . . . 6
wff ( bday ‘𝑦) ∈ ( bday
‘𝑧) |
17 | 12, 16 | wi 4 |
. . . . 5
wff ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday
‘𝑦) ∈
( bday ‘𝑧)) |
18 | 17, 6, 3 | wral 2912 |
. . . 4
wff
∀𝑧 ∈
No ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday
‘𝑦) ∈
( bday ‘𝑧)) |
19 | 10, 13 | cfv 5888 |
. . . . 5
class ( bday ‘𝑥) |
20 | | cold 31926 |
. . . . 5
class
O |
21 | 19, 20 | cfv 5888 |
. . . 4
class ( O
‘( bday ‘𝑥)) |
22 | 18, 4, 21 | crab 2916 |
. . 3
class {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No
((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday
‘𝑦) ∈
( bday ‘𝑧))} |
23 | 2, 3, 22 | cmpt 4729 |
. 2
class (𝑥 ∈
No ↦ {𝑦
∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No
((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday
‘𝑦) ∈
( bday ‘𝑧))}) |
24 | 1, 23 | wceq 1483 |
1
wff L = (𝑥 ∈
No ↦ {𝑦
∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No
((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday
‘𝑦) ∈
( bday ‘𝑧))}) |