Detailed syntax breakdown of Definition df-right
Step | Hyp | Ref
| Expression |
1 | | cright 31929 |
. 2
class
R |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | csur 31793 |
. . 3
class No |
4 | 2 | cv 1482 |
. . . . . . . 8
class 𝑥 |
5 | | vz |
. . . . . . . . 9
setvar 𝑧 |
6 | 5 | cv 1482 |
. . . . . . . 8
class 𝑧 |
7 | | cslt 31794 |
. . . . . . . 8
class
<s |
8 | 4, 6, 7 | wbr 4653 |
. . . . . . 7
wff 𝑥 <s 𝑧 |
9 | | vy |
. . . . . . . . 9
setvar 𝑦 |
10 | 9 | cv 1482 |
. . . . . . . 8
class 𝑦 |
11 | 6, 10, 7 | wbr 4653 |
. . . . . . 7
wff 𝑧 <s 𝑦 |
12 | 8, 11 | wa 384 |
. . . . . 6
wff (𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) |
13 | | cbday 31795 |
. . . . . . . 8
class bday |
14 | 10, 13 | cfv 5888 |
. . . . . . 7
class ( bday ‘𝑦) |
15 | 6, 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, 5, 3 | wral 2912 |
. . . 4
wff
∀𝑧 ∈
No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → ( bday
‘𝑦) ∈
( bday ‘𝑧)) |
19 | 4, 13 | cfv 5888 |
. . . . 5
class ( bday ‘𝑥) |
20 | | cold 31926 |
. . . . 5
class
O |
21 | 19, 20 | cfv 5888 |
. . . 4
class ( O
‘( bday ‘𝑥)) |
22 | 18, 9, 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 R = (𝑥 ∈
No ↦ {𝑦
∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → ( bday
‘𝑦) ∈
( bday ‘𝑧))}) |