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 
|- V = ( Base ` W )
lpolset.s 
|- S = ( LSubSp ` W )
lpolset.z 
|- .0. = ( 0g ` W )
lpolset.a 
|- A = ( LSAtoms ` W )
lpolset.h 
|- H = ( LSHyp ` W )
lpolset.p 
|- P = ( LPol ` W )
Assertion islpolN 
|- ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lpolset.v 
 |-  V = ( Base ` W )
2 lpolset.s 
 |-  S = ( LSubSp ` W )
3 lpolset.z 
 |-  .0. = ( 0g ` W )
4 lpolset.a 
 |-  A = ( LSAtoms ` W )
5 lpolset.h 
 |-  H = ( LSHyp ` W )
6 lpolset.p 
 |-  P = ( LPol ` W )
7 1 2 3 4 5 6 lpolsetN 
 |-  ( W e. X -> P = { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } )
8 7 eleq2d 
 |-  ( W e. X -> ( ._|_ e. P <-> ._|_ e. { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } ) )
9 fveq1 
 |-  ( o = ._|_ -> ( o ` V ) = ( ._|_ ` V ) )
10 9 eqeq1d 
 |-  ( o = ._|_ -> ( ( o ` V ) = { .0. } <-> ( ._|_ ` V ) = { .0. } ) )
11 fveq1 
 |-  ( o = ._|_ -> ( o ` y ) = ( ._|_ ` y ) )
12 fveq1 
 |-  ( o = ._|_ -> ( o ` x ) = ( ._|_ ` x ) )
13 11 12 sseq12d 
 |-  ( o = ._|_ -> ( ( o ` y ) C_ ( o ` x ) <-> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) )
14 13 imbi2d 
 |-  ( o = ._|_ -> ( ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) <-> ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) ) )
15 14 2albidv 
 |-  ( o = ._|_ -> ( A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) <-> A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) ) )
16 12 eleq1d 
 |-  ( o = ._|_ -> ( ( o ` x ) e. H <-> ( ._|_ ` x ) e. H ) )
17 id 
 |-  ( o = ._|_ -> o = ._|_ )
18 17 12 fveq12d 
 |-  ( o = ._|_ -> ( o ` ( o ` x ) ) = ( ._|_ ` ( ._|_ ` x ) ) )
19 18 eqeq1d 
 |-  ( o = ._|_ -> ( ( o ` ( o ` x ) ) = x <-> ( ._|_ ` ( ._|_ ` x ) ) = x ) )
20 16 19 anbi12d 
 |-  ( o = ._|_ -> ( ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) <-> ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) )
21 20 ralbidv 
 |-  ( o = ._|_ -> ( A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) <-> A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) )
22 10 15 21 3anbi123d 
 |-  ( o = ._|_ -> ( ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) <-> ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
23 22 elrab 
 |-  ( ._|_ e. { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } <-> ( ._|_ e. ( S ^m ~P V ) /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
24 2 fvexi 
 |-  S e. _V
25 1 fvexi 
 |-  V e. _V
26 25 pwex 
 |-  ~P V e. _V
27 24 26 elmap 
 |-  ( ._|_ e. ( S ^m ~P V ) <-> ._|_ : ~P V --> S )
28 27 anbi1i 
 |-  ( ( ._|_ e. ( S ^m ~P V ) /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
29 23 28 bitri 
 |-  ( ._|_ e. { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
30 8 29 bitrdi 
 |-  ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )