Detailed syntax breakdown of Definition df-tsr
Step | Hyp | Ref
| Expression |
1 | | ctsr 17246 |
. 2
class
TosetRel |
2 | | vr |
. . . . . . 7
setvar 𝑟 |
3 | 2 | cv 1522 |
. . . . . 6
class 𝑟 |
4 | 3 | cdm 5143 |
. . . . 5
class dom 𝑟 |
5 | 4, 4 | cxp 5141 |
. . . 4
class (dom
𝑟 × dom 𝑟) |
6 | 3 | ccnv 5142 |
. . . . 5
class ◡𝑟 |
7 | 3, 6 | cun 3605 |
. . . 4
class (𝑟 ∪ ◡𝑟) |
8 | 5, 7 | wss 3607 |
. . 3
wff (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟) |
9 | | cps 17245 |
. . 3
class
PosetRel |
10 | 8, 2, 9 | crab 2945 |
. 2
class {𝑟 ∈ PosetRel ∣ (dom
𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} |
11 | 1, 10 | wceq 1523 |
1
wff TosetRel =
{𝑟 ∈ PosetRel ∣
(dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} |