Detailed syntax breakdown of Definition df-drs
Step | Hyp | Ref
| Expression |
1 | | cdrs 18010 |
. 2
class
Dirset |
2 | | vb |
. . . . . . . 8
setvar 𝑏 |
3 | 2 | cv 1538 |
. . . . . . 7
class 𝑏 |
4 | | c0 4258 |
. . . . . . 7
class
∅ |
5 | 3, 4 | wne 2943 |
. . . . . 6
wff 𝑏 ≠ ∅ |
6 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
7 | 6 | cv 1538 |
. . . . . . . . . . 11
class 𝑥 |
8 | | vz |
. . . . . . . . . . . 12
setvar 𝑧 |
9 | 8 | cv 1538 |
. . . . . . . . . . 11
class 𝑧 |
10 | | vr |
. . . . . . . . . . . 12
setvar 𝑟 |
11 | 10 | cv 1538 |
. . . . . . . . . . 11
class 𝑟 |
12 | 7, 9, 11 | wbr 5076 |
. . . . . . . . . 10
wff 𝑥𝑟𝑧 |
13 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
14 | 13 | cv 1538 |
. . . . . . . . . . 11
class 𝑦 |
15 | 14, 9, 11 | wbr 5076 |
. . . . . . . . . 10
wff 𝑦𝑟𝑧 |
16 | 12, 15 | wa 396 |
. . . . . . . . 9
wff (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
17 | 16, 8, 3 | wrex 3065 |
. . . . . . . 8
wff
∃𝑧 ∈
𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
18 | 17, 13, 3 | wral 3064 |
. . . . . . 7
wff
∀𝑦 ∈
𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
19 | 18, 6, 3 | wral 3064 |
. . . . . 6
wff
∀𝑥 ∈
𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) |
20 | 5, 19 | wa 396 |
. . . . 5
wff (𝑏 ≠ ∅ ∧
∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) |
21 | | vf |
. . . . . . 7
setvar 𝑓 |
22 | 21 | cv 1538 |
. . . . . 6
class 𝑓 |
23 | | cple 16967 |
. . . . . 6
class
le |
24 | 22, 23 | cfv 6435 |
. . . . 5
class
(le‘𝑓) |
25 | 20, 10, 24 | wsbc 3717 |
. . . 4
wff
[(le‘𝑓)
/ 𝑟](𝑏 ≠ ∅ ∧
∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) |
26 | | cbs 16910 |
. . . . 5
class
Base |
27 | 22, 26 | cfv 6435 |
. . . 4
class
(Base‘𝑓) |
28 | 25, 2, 27 | wsbc 3717 |
. . 3
wff
[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) |
29 | | cproset 18009 |
. . 3
class
Proset |
30 | 28, 21, 29 | crab 3068 |
. 2
class {𝑓 ∈ Proset ∣
[(Base‘𝑓) /
𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} |
31 | 1, 30 | wceq 1539 |
1
wff Dirset =
{𝑓 ∈ Proset ∣
[(Base‘𝑓) /
𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} |