Detailed syntax breakdown of Definition df-tsr
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ctsr 18071 |
. 2
class
TosetRel |
| 2 | | vr |
. . . . . . 7
setvar 𝑟 |
| 3 | 2 | cv 1542 |
. . . . . 6
class 𝑟 |
| 4 | 3 | cdm 5551 |
. . . . 5
class dom 𝑟 |
| 5 | 4, 4 | cxp 5549 |
. . . 4
class (dom
𝑟 × dom 𝑟) |
| 6 | 3 | ccnv 5550 |
. . . . 5
class ◡𝑟 |
| 7 | 3, 6 | cun 3864 |
. . . 4
class (𝑟 ∪ ◡𝑟) |
| 8 | 5, 7 | wss 3866 |
. . 3
wff (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟) |
| 9 | | cps 18070 |
. . 3
class
PosetRel |
| 10 | 8, 2, 9 | crab 3065 |
. 2
class {𝑟 ∈ PosetRel ∣ (dom
𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} |
| 11 | 1, 10 | wceq 1543 |
1
wff TosetRel =
{𝑟 ∈ PosetRel ∣
(dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} |
