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 39233 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝑃 = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) |
8 | 7 | eleq2d 2823 |
. 2
⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ⊥ ∈ {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})) |
9 | | fveq1 6716 |
. . . . . 6
⊢ (𝑜 = ⊥ → (𝑜‘𝑉) = ( ⊥ ‘𝑉)) |
10 | 9 | eqeq1d 2739 |
. . . . 5
⊢ (𝑜 = ⊥ → ((𝑜‘𝑉) = { 0 } ↔ ( ⊥
‘𝑉) = { 0
})) |
11 | | fveq1 6716 |
. . . . . . . 8
⊢ (𝑜 = ⊥ → (𝑜‘𝑦) = ( ⊥ ‘𝑦)) |
12 | | fveq1 6716 |
. . . . . . . 8
⊢ (𝑜 = ⊥ → (𝑜‘𝑥) = ( ⊥ ‘𝑥)) |
13 | 11, 12 | sseq12d 3934 |
. . . . . . 7
⊢ (𝑜 = ⊥ → ((𝑜‘𝑦) ⊆ (𝑜‘𝑥) ↔ ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥))) |
14 | 13 | imbi2d 344 |
. . . . . 6
⊢ (𝑜 = ⊥ → (((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ↔ ((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)))) |
15 | 14 | 2albidv 1931 |
. . . . 5
⊢ (𝑜 = ⊥ →
(∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ↔ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)))) |
16 | 12 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑜 = ⊥ → ((𝑜‘𝑥) ∈ 𝐻 ↔ ( ⊥ ‘𝑥) ∈ 𝐻)) |
17 | | id 22 |
. . . . . . . . 9
⊢ (𝑜 = ⊥ → 𝑜 = ⊥ ) |
18 | 17, 12 | fveq12d 6724 |
. . . . . . . 8
⊢ (𝑜 = ⊥ → (𝑜‘(𝑜‘𝑥)) = ( ⊥ ‘( ⊥
‘𝑥))) |
19 | 18 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑜 = ⊥ → ((𝑜‘(𝑜‘𝑥)) = 𝑥 ↔ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)) |
20 | 16, 19 | anbi12d 634 |
. . . . . 6
⊢ (𝑜 = ⊥ → (((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) ↔ (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) |
21 | 20 | ralbidv 3118 |
. . . . 5
⊢ (𝑜 = ⊥ →
(∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥) ↔ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) |
22 | 10, 15, 21 | 3anbi123d 1438 |
. . . 4
⊢ (𝑜 = ⊥ → (((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)) ↔ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
23 | 22 | elrab 3602 |
. . 3
⊢ ( ⊥ ∈
{𝑜 ∈ (𝑆 ↑m 𝒫
𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))} ↔ ( ⊥ ∈ (𝑆 ↑m 𝒫
𝑉) ∧ (( ⊥
‘𝑉) = { 0 } ∧
∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
24 | 2 | fvexi 6731 |
. . . . 5
⊢ 𝑆 ∈ V |
25 | 1 | fvexi 6731 |
. . . . . 6
⊢ 𝑉 ∈ V |
26 | 25 | pwex 5273 |
. . . . 5
⊢ 𝒫
𝑉 ∈ V |
27 | 24, 26 | elmap 8552 |
. . . 4
⊢ ( ⊥ ∈
(𝑆 ↑m
𝒫 𝑉) ↔ ⊥
:𝒫 𝑉⟶𝑆) |
28 | 27 | anbi1i 627 |
. . 3
⊢ (( ⊥ ∈
(𝑆 ↑m
𝒫 𝑉) ∧ (( ⊥
‘𝑉) = { 0 } ∧
∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
29 | 23, 28 | bitri 278 |
. 2
⊢ ( ⊥ ∈
{𝑜 ∈ (𝑆 ↑m 𝒫
𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))} ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
30 | 8, 29 | bitrdi 290 |
1
⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) |