Detailed syntax breakdown of Definition df-drs
| Step | Hyp | Ref
| Expression |
| 1 | | cdrs 18339 |
. 2
class
Dirset |
| 2 | | vb |
. . . . . . . 8
setvar 𝑏 |
| 3 | 2 | cv 1539 |
. . . . . . 7
class 𝑏 |
| 4 | | c0 4333 |
. . . . . . 7
class
∅ |
| 5 | 3, 4 | wne 2940 |
. . . . . 6
wff 𝑏 ≠ ∅ |
| 6 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
| 7 | 6 | cv 1539 |
. . . . . . . . . . 11
class 𝑥 |
| 8 | | vz |
. . . . . . . . . . . 12
setvar 𝑧 |
| 9 | 8 | cv 1539 |
. . . . . . . . . . 11
class 𝑧 |
| 10 | | vr |
. . . . . . . . . . . 12
setvar 𝑟 |
| 11 | 10 | cv 1539 |
. . . . . . . . . . 11
class 𝑟 |
| 12 | 7, 9, 11 | wbr 5143 |
. . . . . . . . . 10
wff 𝑥𝑟𝑧 |
| 13 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
| 14 | 13 | cv 1539 |
. . . . . . . . . . 11
class 𝑦 |
| 15 | 14, 9, 11 | wbr 5143 |
. . . . . . . . . 10
wff 𝑦𝑟𝑧 |
| 16 | 12, 15 | wa 395 |
. . . . . . . . 9
wff (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
| 17 | 16, 8, 3 | wrex 3070 |
. . . . . . . 8
wff
∃𝑧 ∈
𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
| 18 | 17, 13, 3 | wral 3061 |
. . . . . . 7
wff
∀𝑦 ∈
𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
| 19 | 18, 6, 3 | wral 3061 |
. . . . . 6
wff
∀𝑥 ∈
𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
| 20 | 5, 19 | wa 395 |
. . . . 5
wff (𝑏 ≠ ∅ ∧
∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) |
| 21 | | vf |
. . . . . . 7
setvar 𝑓 |
| 22 | 21 | cv 1539 |
. . . . . 6
class 𝑓 |
| 23 | | cple 17304 |
. . . . . 6
class
le |
| 24 | 22, 23 | cfv 6561 |
. . . . 5
class
(le‘𝑓) |
| 25 | 20, 10, 24 | wsbc 3788 |
. . . 4
wff
[(le‘𝑓)
/ 𝑟](𝑏 ≠ ∅ ∧
∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) |
| 26 | | cbs 17247 |
. . . . 5
class
Base |
| 27 | 22, 26 | cfv 6561 |
. . . 4
class
(Base‘𝑓) |
| 28 | 25, 2, 27 | wsbc 3788 |
. . 3
wff
[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) |
| 29 | | cproset 18338 |
. . 3
class
Proset |
| 30 | 28, 21, 29 | crab 3436 |
. 2
class {𝑓 ∈ Proset ∣
[(Base‘𝑓) /
𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} |
| 31 | 1, 30 | wceq 1540 |
1
wff Dirset =
{𝑓 ∈ Proset ∣
[(Base‘𝑓) /
𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} |