Detailed syntax breakdown of Definition df-ordt
Step | Hyp | Ref
| Expression |
1 | | cordt 17004 |
. 2
class
ordTop |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | cvv 3408 |
. . 3
class
V |
4 | 2 | cv 1542 |
. . . . . . . 8
class 𝑟 |
5 | 4 | cdm 5551 |
. . . . . . 7
class dom 𝑟 |
6 | 5 | csn 4541 |
. . . . . 6
class {dom
𝑟} |
7 | | vx |
. . . . . . . . 9
setvar 𝑥 |
8 | | vy |
. . . . . . . . . . . . 13
setvar 𝑦 |
9 | 8 | cv 1542 |
. . . . . . . . . . . 12
class 𝑦 |
10 | 7 | cv 1542 |
. . . . . . . . . . . 12
class 𝑥 |
11 | 9, 10, 4 | wbr 5053 |
. . . . . . . . . . 11
wff 𝑦𝑟𝑥 |
12 | 11 | wn 3 |
. . . . . . . . . 10
wff ¬
𝑦𝑟𝑥 |
13 | 12, 8, 5 | crab 3065 |
. . . . . . . . 9
class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥} |
14 | 7, 5, 13 | cmpt 5135 |
. . . . . . . 8
class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) |
15 | 10, 9, 4 | wbr 5053 |
. . . . . . . . . . 11
wff 𝑥𝑟𝑦 |
16 | 15 | wn 3 |
. . . . . . . . . 10
wff ¬
𝑥𝑟𝑦 |
17 | 16, 8, 5 | crab 3065 |
. . . . . . . . 9
class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦} |
18 | 7, 5, 17 | cmpt 5135 |
. . . . . . . 8
class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}) |
19 | 14, 18 | cun 3864 |
. . . . . . 7
class ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})) |
20 | 19 | crn 5552 |
. . . . . 6
class ran
((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})) |
21 | 6, 20 | cun 3864 |
. . . . 5
class ({dom
𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))) |
22 | | cfi 9026 |
. . . . 5
class
fi |
23 | 21, 22 | cfv 6380 |
. . . 4
class
(fi‘({dom 𝑟}
∪ ran ((𝑥 ∈ dom
𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))) |
24 | | ctg 16942 |
. . . 4
class
topGen |
25 | 23, 24 | cfv 6380 |
. . 3
class
(topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))) |
26 | 2, 3, 25 | cmpt 5135 |
. 2
class (𝑟 ∈ V ↦
(topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))) |
27 | 1, 26 | wceq 1543 |
1
wff ordTop =
(𝑟 ∈ V ↦
(topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))) |