Detailed syntax breakdown of Definition df-lnm
| Step | Hyp | Ref
| Expression |
| 1 | | clnm 43087 |
. 2
class
LNoeM |
| 2 | | vw |
. . . . . . 7
setvar 𝑤 |
| 3 | 2 | cv 1539 |
. . . . . 6
class 𝑤 |
| 4 | | vi |
. . . . . . 7
setvar 𝑖 |
| 5 | 4 | cv 1539 |
. . . . . 6
class 𝑖 |
| 6 | | cress 17274 |
. . . . . 6
class
↾s |
| 7 | 3, 5, 6 | co 7431 |
. . . . 5
class (𝑤 ↾s 𝑖) |
| 8 | | clfig 43079 |
. . . . 5
class
LFinGen |
| 9 | 7, 8 | wcel 2108 |
. . . 4
wff (𝑤 ↾s 𝑖) ∈
LFinGen |
| 10 | | clss 20929 |
. . . . 5
class
LSubSp |
| 11 | 3, 10 | cfv 6561 |
. . . 4
class
(LSubSp‘𝑤) |
| 12 | 9, 4, 11 | wral 3061 |
. . 3
wff
∀𝑖 ∈
(LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈
LFinGen |
| 13 | | clmod 20858 |
. . 3
class
LMod |
| 14 | 12, 2, 13 | crab 3436 |
. 2
class {𝑤 ∈ LMod ∣
∀𝑖 ∈
(LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈
LFinGen} |
| 15 | 1, 14 | wceq 1540 |
1
wff LNoeM =
{𝑤 ∈ LMod ∣
∀𝑖 ∈
(LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈
LFinGen} |