Detailed syntax breakdown of Definition df-asp
Step | Hyp | Ref
| Expression |
1 | | casp 21068 |
. 2
class
AlgSpan |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | casa 21067 |
. . 3
class
AssAlg |
4 | | vs |
. . . 4
setvar 𝑠 |
5 | 2 | cv 1538 |
. . . . . 6
class 𝑤 |
6 | | cbs 16922 |
. . . . . 6
class
Base |
7 | 5, 6 | cfv 6426 |
. . . . 5
class
(Base‘𝑤) |
8 | 7 | cpw 4533 |
. . . 4
class 𝒫
(Base‘𝑤) |
9 | 4 | cv 1538 |
. . . . . . 7
class 𝑠 |
10 | | vt |
. . . . . . . 8
setvar 𝑡 |
11 | 10 | cv 1538 |
. . . . . . 7
class 𝑡 |
12 | 9, 11 | wss 3886 |
. . . . . 6
wff 𝑠 ⊆ 𝑡 |
13 | | csubrg 20030 |
. . . . . . . 8
class
SubRing |
14 | 5, 13 | cfv 6426 |
. . . . . . 7
class
(SubRing‘𝑤) |
15 | | clss 20203 |
. . . . . . . 8
class
LSubSp |
16 | 5, 15 | cfv 6426 |
. . . . . . 7
class
(LSubSp‘𝑤) |
17 | 14, 16 | cin 3885 |
. . . . . 6
class
((SubRing‘𝑤)
∩ (LSubSp‘𝑤)) |
18 | 12, 10, 17 | crab 3068 |
. . . . 5
class {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} |
19 | 18 | cint 4879 |
. . . 4
class ∩ {𝑡
∈ ((SubRing‘𝑤)
∩ (LSubSp‘𝑤))
∣ 𝑠 ⊆ 𝑡} |
20 | 4, 8, 19 | cmpt 5156 |
. . 3
class (𝑠 ∈ 𝒫
(Base‘𝑤) ↦
∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}) |
21 | 2, 3, 20 | cmpt 5156 |
. 2
class (𝑤 ∈ AssAlg ↦ (𝑠 ∈ 𝒫
(Base‘𝑤) ↦
∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})) |
22 | 1, 21 | wceq 1539 |
1
wff AlgSpan =
(𝑤 ∈ AssAlg ↦
(𝑠 ∈ 𝒫
(Base‘𝑤) ↦
∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})) |