Detailed syntax breakdown of Definition df-tsr
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ctsr 17404 |
. 2
class
TosetRel |
| 2 | | vr |
. . . . . . 7
setvar 𝑟 |
| 3 | 2 | cv 1636 |
. . . . . 6
class 𝑟 |
| 4 | 3 | cdm 5311 |
. . . . 5
class dom 𝑟 |
| 5 | 4, 4 | cxp 5309 |
. . . 4
class (dom
𝑟 × dom 𝑟) |
| 6 | 3 | ccnv 5310 |
. . . . 5
class ◡𝑟 |
| 7 | 3, 6 | cun 3767 |
. . . 4
class (𝑟 ∪ ◡𝑟) |
| 8 | 5, 7 | wss 3769 |
. . 3
wff (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟) |
| 9 | | cps 17403 |
. . 3
class
PosetRel |
| 10 | 8, 2, 9 | crab 3100 |
. 2
class {𝑟 ∈ PosetRel ∣ (dom
𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} |
| 11 | 1, 10 | wceq 1637 |
1
wff TosetRel =
{𝑟 ∈ PosetRel ∣
(dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} |
