Detailed syntax breakdown of Definition df-lvols
Step | Hyp | Ref
| Expression |
1 | | clvol 37119 |
. 2
class
LVols |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3397 |
. . 3
class
V |
4 | | vp |
. . . . . . 7
setvar 𝑝 |
5 | 4 | cv 1541 |
. . . . . 6
class 𝑝 |
6 | | vx |
. . . . . . 7
setvar 𝑥 |
7 | 6 | cv 1541 |
. . . . . 6
class 𝑥 |
8 | 2 | cv 1541 |
. . . . . . 7
class 𝑘 |
9 | | ccvr 36888 |
. . . . . . 7
class
⋖ |
10 | 8, 9 | cfv 6333 |
. . . . . 6
class ( ⋖
‘𝑘) |
11 | 5, 7, 10 | wbr 5027 |
. . . . 5
wff 𝑝( ⋖ ‘𝑘)𝑥 |
12 | | clpl 37118 |
. . . . . 6
class
LPlanes |
13 | 8, 12 | cfv 6333 |
. . . . 5
class
(LPlanes‘𝑘) |
14 | 11, 4, 13 | wrex 3054 |
. . . 4
wff
∃𝑝 ∈
(LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥 |
15 | | cbs 16579 |
. . . . 5
class
Base |
16 | 8, 15 | cfv 6333 |
. . . 4
class
(Base‘𝑘) |
17 | 14, 6, 16 | crab 3057 |
. . 3
class {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥} |
18 | 2, 3, 17 | cmpt 5107 |
. 2
class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥}) |
19 | 1, 18 | wceq 1542 |
1
wff LVols =
(𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥}) |