| Step | Hyp | Ref
| Expression |
| 1 | | lpolset.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
| 2 | | lpolset.s |
. . . 4
⊢ 𝑆 = (LSubSp‘𝑊) |
| 3 | | lpolset.z |
. . . 4
⊢ 0 =
(0g‘𝑊) |
| 4 | | lpolset.a |
. . . 4
⊢ 𝐴 = (LSAtoms‘𝑊) |
| 5 | | lpolset.h |
. . . 4
⊢ 𝐻 = (LSHyp‘𝑊) |
| 6 | | lpolset.p |
. . . 4
⊢ 𝑃 = (LPol‘𝑊) |
| 7 | 1, 2, 3, 4, 5, 6 | lpolsetN 41484 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝑃 = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |
| 8 | 7 | eleq2d 2827 |
. 2
⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ⊥ ∈ {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})) |
| 9 | | fveq1 6905 |
. . . . . 6
⊢ (𝑜 = ⊥ → (𝑜‘𝑉) = ( ⊥ ‘𝑉)) |
| 10 | 9 | eqeq1d 2739 |
. . . . 5
⊢ (𝑜 = ⊥ → ((𝑜‘𝑉) = { 0 } ↔ ( ⊥
‘𝑉) = { 0
})) |
| 11 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑜 = ⊥ → (𝑜‘𝑦) = ( ⊥ ‘𝑦)) |
| 12 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑜 = ⊥ → (𝑜‘𝑥) = ( ⊥ ‘𝑥)) |
| 13 | 11, 12 | sseq12d 4017 |
. . . . . . 7
⊢ (𝑜 = ⊥ → ((𝑜‘𝑦) ⊆ (𝑜‘𝑥) ↔ ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥))) |
| 14 | 13 | imbi2d 340 |
. . . . . 6
⊢ (𝑜 = ⊥ → (((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ↔ ((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)))) |
| 15 | 14 | 2albidv 1923 |
. . . . 5
⊢ (𝑜 = ⊥ →
(∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ↔ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)))) |
| 16 | 12 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑜 = ⊥ → ((𝑜‘𝑥) ∈ 𝐻 ↔ ( ⊥ ‘𝑥) ∈ 𝐻)) |
| 17 | | id 22 |
. . . . . . . . 9
⊢ (𝑜 = ⊥ → 𝑜 = ⊥ ) |
| 18 | 17, 12 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑜 = ⊥ → (𝑜‘(𝑜‘𝑥)) = ( ⊥ ‘( ⊥
‘𝑥))) |
| 19 | 18 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑜 = ⊥ → ((𝑜‘(𝑜‘𝑥)) = 𝑥 ↔ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)) |
| 20 | 16, 19 | anbi12d 632 |
. . . . . 6
⊢ (𝑜 = ⊥ → (((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) ↔ (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) |
| 21 | 20 | ralbidv 3178 |
. . . . 5
⊢ (𝑜 = ⊥ →
(∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) ↔ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) |
| 22 | 10, 15, 21 | 3anbi123d 1438 |
. . . 4
⊢ (𝑜 = ⊥ → (((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)) ↔ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
| 23 | 22 | elrab 3692 |
. . 3
⊢ ( ⊥ ∈
{𝑜 ∈ (𝑆 ↑m 𝒫
𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))} ↔ ( ⊥ ∈ (𝑆 ↑m 𝒫
𝑉) ∧ (( ⊥
‘𝑉) = { 0 } ∧
∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
| 24 | 2 | fvexi 6920 |
. . . . 5
⊢ 𝑆 ∈ V |
| 25 | 1 | fvexi 6920 |
. . . . . 6
⊢ 𝑉 ∈ V |
| 26 | 25 | pwex 5380 |
. . . . 5
⊢ 𝒫
𝑉 ∈ V |
| 27 | 24, 26 | elmap 8911 |
. . . 4
⊢ ( ⊥ ∈
(𝑆 ↑m
𝒫 𝑉) ↔ ⊥
:𝒫 𝑉⟶𝑆) |
| 28 | 27 | anbi1i 624 |
. . 3
⊢ (( ⊥ ∈
(𝑆 ↑m
𝒫 𝑉) ∧ (( ⊥
‘𝑉) = { 0 } ∧
∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
| 29 | 23, 28 | bitri 275 |
. 2
⊢ ( ⊥ ∈
{𝑜 ∈ (𝑆 ↑m 𝒫
𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))} ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
| 30 | 8, 29 | bitrdi 287 |
1
⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) |