| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
| 2 | | lpolset.p |
. . 3
⊢ 𝑃 = (LPol‘𝑊) |
| 3 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
| 4 | | lpolset.s |
. . . . . . 7
⊢ 𝑆 = (LSubSp‘𝑊) |
| 5 | 3, 4 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝑆) |
| 6 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
| 7 | | lpolset.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
| 9 | 8 | pweqd 4617 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉) |
| 10 | 5, 9 | oveq12d 7449 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((LSubSp‘𝑤) ↑m 𝒫
(Base‘𝑤)) = (𝑆 ↑m 𝒫
𝑉)) |
| 11 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑜‘(Base‘𝑤)) = (𝑜‘𝑉)) |
| 12 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊)) |
| 13 | | lpolset.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑊) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 ) |
| 15 | 14 | sneqd 4638 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 }) |
| 16 | 11, 15 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ↔ (𝑜‘𝑉) = { 0 })) |
| 17 | 8 | sseq2d 4016 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑥 ⊆ (Base‘𝑤) ↔ 𝑥 ⊆ 𝑉)) |
| 18 | 8 | sseq2d 4016 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑦 ⊆ (Base‘𝑤) ↔ 𝑦 ⊆ 𝑉)) |
| 19 | 17, 18 | 3anbi12d 1439 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) ↔ (𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦))) |
| 20 | 19 | imbi1d 341 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ↔ ((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)))) |
| 21 | 20 | 2albidv 1923 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ↔ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)))) |
| 22 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSAtoms‘𝑤) = (LSAtoms‘𝑊)) |
| 23 | | lpolset.a |
. . . . . . . 8
⊢ 𝐴 = (LSAtoms‘𝑊) |
| 24 | 22, 23 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (LSAtoms‘𝑤) = 𝐴) |
| 25 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (LSHyp‘𝑤) = (LSHyp‘𝑊)) |
| 26 | | lpolset.h |
. . . . . . . . . 10
⊢ 𝐻 = (LSHyp‘𝑊) |
| 27 | 25, 26 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (LSHyp‘𝑤) = 𝐻) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ↔ (𝑜‘𝑥) ∈ 𝐻)) |
| 29 | 28 | anbi1d 631 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) ↔ ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))) |
| 30 | 24, 29 | raleqbidv 3346 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) ↔ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))) |
| 31 | 16, 21, 30 | 3anbi123d 1438 |
. . . . 5
⊢ (𝑤 = 𝑊 → (((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)) ↔ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)))) |
| 32 | 10, 31 | rabeqbidv 3455 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫
(Base‘𝑤)) ∣
((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))} = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |
| 33 | | df-lpolN 41483 |
. . . 4
⊢ LPol =
(𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫
(Base‘𝑤)) ∣
((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |
| 34 | | ovex 7464 |
. . . . 5
⊢ (𝑆 ↑m 𝒫
𝑉) ∈
V |
| 35 | 34 | rabex 5339 |
. . . 4
⊢ {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))} ∈ V |
| 36 | 32, 33, 35 | fvmpt 7016 |
. . 3
⊢ (𝑊 ∈ V →
(LPol‘𝑊) = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |
| 37 | 2, 36 | eqtrid 2789 |
. 2
⊢ (𝑊 ∈ V → 𝑃 = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |
| 38 | 1, 37 | syl 17 |
1
⊢ (𝑊 ∈ 𝑋 → 𝑃 = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |