Metamath Proof Explorer


Theorem islpolN

Description: The predicate "is a polarity". (Contributed by NM, 24-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolset.v 𝑉 = ( Base ‘ 𝑊 )
lpolset.s 𝑆 = ( LSubSp ‘ 𝑊 )
lpolset.z 0 = ( 0g𝑊 )
lpolset.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lpolset.h 𝐻 = ( LSHyp ‘ 𝑊 )
lpolset.p 𝑃 = ( LPol ‘ 𝑊 )
Assertion islpolN ( 𝑊𝑋 → ( 𝑃 ↔ ( : 𝒫 𝑉𝑆 ∧ ( ( 𝑉 ) = { 0 } ∧ ∀ 𝑥𝑦 ( ( 𝑥𝑉𝑦𝑉𝑥𝑦 ) → ( 𝑦 ) ⊆ ( 𝑥 ) ) ∧ ∀ 𝑥𝐴 ( ( 𝑥 ) ∈ 𝐻 ∧ ( ‘ ( 𝑥 ) ) = 𝑥 ) ) ) ) )

Proof

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 } ∧ ∀ 𝑥𝑦 ( ( 𝑥𝑉𝑦𝑉𝑥𝑦 ) → ( 𝑦 ) ⊆ ( 𝑥 ) ) ∧ ∀ 𝑥𝐴 ( ( 𝑥 ) ∈ 𝐻 ∧ ( ‘ ( 𝑥 ) ) = 𝑥 ) ) ) ) )