Detailed syntax breakdown of Definition df-sslt
Step | Hyp | Ref
| Expression |
1 | | csslt 33631 |
. 2
class
<<s |
2 | | va |
. . . . . 6
setvar 𝑎 |
3 | 2 | cv 1541 |
. . . . 5
class 𝑎 |
4 | | csur 33499 |
. . . . 5
class No |
5 | 3, 4 | wss 3853 |
. . . 4
wff 𝑎 ⊆
No |
6 | | vb |
. . . . . 6
setvar 𝑏 |
7 | 6 | cv 1541 |
. . . . 5
class 𝑏 |
8 | 7, 4 | wss 3853 |
. . . 4
wff 𝑏 ⊆
No |
9 | | vx |
. . . . . . . 8
setvar 𝑥 |
10 | 9 | cv 1541 |
. . . . . . 7
class 𝑥 |
11 | | vy |
. . . . . . . 8
setvar 𝑦 |
12 | 11 | cv 1541 |
. . . . . . 7
class 𝑦 |
13 | | cslt 33500 |
. . . . . . 7
class
<s |
14 | 10, 12, 13 | wbr 5040 |
. . . . . 6
wff 𝑥 <s 𝑦 |
15 | 14, 11, 7 | wral 3054 |
. . . . 5
wff
∀𝑦 ∈
𝑏 𝑥 <s 𝑦 |
16 | 15, 9, 3 | wral 3054 |
. . . 4
wff
∀𝑥 ∈
𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦 |
17 | 5, 8, 16 | w3a 1088 |
. . 3
wff (𝑎 ⊆
No ∧ 𝑏 ⊆
No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦) |
18 | 17, 2, 6 | copab 5102 |
. 2
class
{〈𝑎, 𝑏〉 ∣ (𝑎 ⊆
No ∧ 𝑏 ⊆
No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)} |
19 | 1, 18 | wceq 1542 |
1
wff <<s
= {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆
No ∧ 𝑏 ⊆
No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)} |