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 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} |
