Detailed syntax breakdown of Definition df-lpolN
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | clpoN 41482 | . 2
class
LPol | 
| 2 |  | vw | . . 3
setvar 𝑤 | 
| 3 |  | cvv 3480 | . . 3
class
V | 
| 4 | 2 | cv 1539 | . . . . . . . 8
class 𝑤 | 
| 5 |  | cbs 17247 | . . . . . . . 8
class
Base | 
| 6 | 4, 5 | cfv 6561 | . . . . . . 7
class
(Base‘𝑤) | 
| 7 |  | vo | . . . . . . . 8
setvar 𝑜 | 
| 8 | 7 | cv 1539 | . . . . . . 7
class 𝑜 | 
| 9 | 6, 8 | cfv 6561 | . . . . . 6
class (𝑜‘(Base‘𝑤)) | 
| 10 |  | c0g 17484 | . . . . . . . 8
class
0g | 
| 11 | 4, 10 | cfv 6561 | . . . . . . 7
class
(0g‘𝑤) | 
| 12 | 11 | csn 4626 | . . . . . 6
class
{(0g‘𝑤)} | 
| 13 | 9, 12 | wceq 1540 | . . . . 5
wff (𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} | 
| 14 |  | vx | . . . . . . . . . . 11
setvar 𝑥 | 
| 15 | 14 | cv 1539 | . . . . . . . . . 10
class 𝑥 | 
| 16 | 15, 6 | wss 3951 | . . . . . . . . 9
wff 𝑥 ⊆ (Base‘𝑤) | 
| 17 |  | vy | . . . . . . . . . . 11
setvar 𝑦 | 
| 18 | 17 | cv 1539 | . . . . . . . . . 10
class 𝑦 | 
| 19 | 18, 6 | wss 3951 | . . . . . . . . 9
wff 𝑦 ⊆ (Base‘𝑤) | 
| 20 | 15, 18 | wss 3951 | . . . . . . . . 9
wff 𝑥 ⊆ 𝑦 | 
| 21 | 16, 19, 20 | w3a 1087 | . . . . . . . 8
wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) | 
| 22 | 18, 8 | cfv 6561 | . . . . . . . . 9
class (𝑜‘𝑦) | 
| 23 | 15, 8 | cfv 6561 | . . . . . . . . 9
class (𝑜‘𝑥) | 
| 24 | 22, 23 | wss 3951 | . . . . . . . 8
wff (𝑜‘𝑦) ⊆ (𝑜‘𝑥) | 
| 25 | 21, 24 | wi 4 | . . . . . . 7
wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) | 
| 26 | 25, 17 | wal 1538 | . . . . . 6
wff
∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) | 
| 27 | 26, 14 | wal 1538 | . . . . 5
wff
∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) | 
| 28 |  | clsh 38976 | . . . . . . . . 9
class
LSHyp | 
| 29 | 4, 28 | cfv 6561 | . . . . . . . 8
class
(LSHyp‘𝑤) | 
| 30 | 23, 29 | wcel 2108 | . . . . . . 7
wff (𝑜‘𝑥) ∈ (LSHyp‘𝑤) | 
| 31 | 23, 8 | cfv 6561 | . . . . . . . 8
class (𝑜‘(𝑜‘𝑥)) | 
| 32 | 31, 15 | wceq 1540 | . . . . . . 7
wff (𝑜‘(𝑜‘𝑥)) = 𝑥 | 
| 33 | 30, 32 | wa 395 | . . . . . 6
wff ((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) | 
| 34 |  | clsa 38975 | . . . . . . 7
class
LSAtoms | 
| 35 | 4, 34 | cfv 6561 | . . . . . 6
class
(LSAtoms‘𝑤) | 
| 36 | 33, 14, 35 | wral 3061 | . . . . 5
wff
∀𝑥 ∈
(LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) | 
| 37 | 13, 27, 36 | w3a 1087 | . . . 4
wff ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)) | 
| 38 |  | clss 20929 | . . . . . 6
class
LSubSp | 
| 39 | 4, 38 | cfv 6561 | . . . . 5
class
(LSubSp‘𝑤) | 
| 40 | 6 | cpw 4600 | . . . . 5
class 𝒫
(Base‘𝑤) | 
| 41 |  | cmap 8866 | . . . . 5
class 
↑m | 
| 42 | 39, 40, 41 | co 7431 | . . . 4
class
((LSubSp‘𝑤)
↑m 𝒫 (Base‘𝑤)) | 
| 43 | 37, 7, 42 | crab 3436 | . . 3
class {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫
(Base‘𝑤)) ∣
((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))} | 
| 44 | 2, 3, 43 | cmpt 5225 | . 2
class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫
(Base‘𝑤)) ∣
((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) | 
| 45 | 1, 44 | wceq 1540 | 1
wff LPol =
(𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫
(Base‘𝑤)) ∣
((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |