Detailed syntax breakdown of Definition df-slt
Step | Hyp | Ref
| Expression |
1 | | cslt 31038 |
. 2
class
<s |
2 | | vf |
. . . . . . 7
setvar 𝑓 |
3 | 2 | cv 1474 |
. . . . . 6
class 𝑓 |
4 | | csur 31037 |
. . . . . 6
class No |
5 | 3, 4 | wcel 1977 |
. . . . 5
wff 𝑓 ∈
No |
6 | | vg |
. . . . . . 7
setvar 𝑔 |
7 | 6 | cv 1474 |
. . . . . 6
class 𝑔 |
8 | 7, 4 | wcel 1977 |
. . . . 5
wff 𝑔 ∈
No |
9 | 5, 8 | wa 383 |
. . . 4
wff (𝑓 ∈
No ∧ 𝑔 ∈
No ) |
10 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
11 | 10 | cv 1474 |
. . . . . . . . 9
class 𝑦 |
12 | 11, 3 | cfv 5804 |
. . . . . . . 8
class (𝑓‘𝑦) |
13 | 11, 7 | cfv 5804 |
. . . . . . . 8
class (𝑔‘𝑦) |
14 | 12, 13 | wceq 1475 |
. . . . . . 7
wff (𝑓‘𝑦) = (𝑔‘𝑦) |
15 | | vx |
. . . . . . . 8
setvar 𝑥 |
16 | 15 | cv 1474 |
. . . . . . 7
class 𝑥 |
17 | 14, 10, 16 | wral 2896 |
. . . . . 6
wff
∀𝑦 ∈
𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) |
18 | 16, 3 | cfv 5804 |
. . . . . . 7
class (𝑓‘𝑥) |
19 | 16, 7 | cfv 5804 |
. . . . . . 7
class (𝑔‘𝑥) |
20 | | c1o 7440 |
. . . . . . . . 9
class
1𝑜 |
21 | | c0 3874 |
. . . . . . . . 9
class
∅ |
22 | 20, 21 | cop 4131 |
. . . . . . . 8
class
〈1𝑜, ∅〉 |
23 | | c2o 7441 |
. . . . . . . . 9
class
2𝑜 |
24 | 20, 23 | cop 4131 |
. . . . . . . 8
class
〈1𝑜,
2𝑜〉 |
25 | 21, 23 | cop 4131 |
. . . . . . . 8
class
〈∅, 2𝑜〉 |
26 | 22, 24, 25 | ctp 4129 |
. . . . . . 7
class
{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} |
27 | 18, 19, 26 | wbr 4583 |
. . . . . 6
wff (𝑓‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝑔‘𝑥) |
28 | 17, 27 | wa 383 |
. . . . 5
wff
(∀𝑦 ∈
𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝑔‘𝑥)) |
29 | | con0 5640 |
. . . . 5
class
On |
30 | 28, 15, 29 | wrex 2897 |
. . . 4
wff
∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝑔‘𝑥)) |
31 | 9, 30 | wa 383 |
. . 3
wff ((𝑓 ∈
No ∧ 𝑔 ∈
No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝑔‘𝑥))) |
32 | 31, 2, 6 | copab 4642 |
. 2
class
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈
No ∧ 𝑔 ∈
No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝑔‘𝑥)))} |
33 | 1, 32 | wceq 1475 |
1
wff <s =
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈
No ∧ 𝑔 ∈
No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝑔‘𝑥)))} |