Detailed syntax breakdown of Definition df-llines
Step | Hyp | Ref
| Expression |
1 | | clln 37501 |
. 2
class
LLines |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3431 |
. . 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 37272 |
. . . . . . 7
class
⋖ |
10 | 8, 9 | cfv 6432 |
. . . . . 6
class ( ⋖
‘𝑘) |
11 | 5, 7, 10 | wbr 5079 |
. . . . 5
wff 𝑝( ⋖ ‘𝑘)𝑥 |
12 | | catm 37273 |
. . . . . 6
class
Atoms |
13 | 8, 12 | cfv 6432 |
. . . . 5
class
(Atoms‘𝑘) |
14 | 11, 4, 13 | wrex 3067 |
. . . 4
wff
∃𝑝 ∈
(Atoms‘𝑘)𝑝( ⋖ ‘𝑘)𝑥 |
15 | | cbs 16910 |
. . . . 5
class
Base |
16 | 8, 15 | cfv 6432 |
. . . 4
class
(Base‘𝑘) |
17 | 14, 6, 16 | crab 3070 |
. . 3
class {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑝( ⋖ ‘𝑘)𝑥} |
18 | 2, 3, 17 | cmpt 5162 |
. 2
class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑝( ⋖ ‘𝑘)𝑥}) |
19 | 1, 18 | wceq 1542 |
1
wff LLines =
(𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑝( ⋖ ‘𝑘)𝑥}) |