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