Metamath Proof Explorer

Theorem lpolconN

Description: Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolcon.v 
|- V = ( Base ` W )
lpolcon.p 
|- P = ( LPol ` W )
lpolcon.w 
|- ( ph -> W e. X )
lpolcon.o 
|- ( ph -> ._|_ e. P )
lpolcon.x 
|- ( ph -> X C_ V )
lpolcon.y 
|- ( ph -> Y C_ V )
lpolcon.c 
|- ( ph -> X C_ Y )
Assertion lpolconN 
|- ( ph -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) )

Proof

Step Hyp Ref Expression
1 lpolcon.v 
 |-  V = ( Base ` W )
2 lpolcon.p 
 |-  P = ( LPol ` W )
3 lpolcon.w 
 |-  ( ph -> W e. X )
4 lpolcon.o 
 |-  ( ph -> ._|_ e. P )
5 lpolcon.x 
 |-  ( ph -> X C_ V )
6 lpolcon.y 
 |-  ( ph -> Y C_ V )
7 lpolcon.c 
 |-  ( ph -> X C_ Y )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
10 eqid 
 |-  ( LSAtoms ` W ) = ( LSAtoms ` W )
11 eqid 
 |-  ( LSHyp ` W ) = ( LSHyp ` W )
12 1 8 9 10 11 2 islpolN 
 |-  ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
13 3 12 syl 
 |-  ( ph -> ( ._|_ e. P <-> ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
14 4 13 mpbid 
 |-  ( ph -> ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
15 simpr2 
 |-  ( ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) -> A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) )
16 5 6 7 3jca 
 |-  ( ph -> ( X C_ V /\ Y C_ V /\ X C_ Y ) )
17 1 fvexi 
 |-  V e. _V
18 17 elpw2 
 |-  ( X e. ~P V <-> X C_ V )
19 5 18 sylibr 
 |-  ( ph -> X e. ~P V )
20 17 elpw2 
 |-  ( Y e. ~P V <-> Y C_ V )
21 6 20 sylibr 
 |-  ( ph -> Y e. ~P V )
22 sseq1 
 |-  ( x = X -> ( x C_ V <-> X C_ V ) )
23 biidd 
 |-  ( x = X -> ( y C_ V <-> y C_ V ) )
24 sseq1 
 |-  ( x = X -> ( x C_ y <-> X C_ y ) )
25 22 23 24 3anbi123d 
 |-  ( x = X -> ( ( x C_ V /\ y C_ V /\ x C_ y ) <-> ( X C_ V /\ y C_ V /\ X C_ y ) ) )
26 fveq2 
 |-  ( x = X -> ( ._|_ ` x ) = ( ._|_ ` X ) )
27 26 sseq2d 
 |-  ( x = X -> ( ( ._|_ ` y ) C_ ( ._|_ ` x ) <-> ( ._|_ ` y ) C_ ( ._|_ ` X ) ) )
28 25 27 imbi12d 
 |-  ( x = X -> ( ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) <-> ( ( X C_ V /\ y C_ V /\ X C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` X ) ) ) )
29 biidd 
 |-  ( y = Y -> ( X C_ V <-> X C_ V ) )
30 sseq1 
 |-  ( y = Y -> ( y C_ V <-> Y C_ V ) )
31 sseq2 
 |-  ( y = Y -> ( X C_ y <-> X C_ Y ) )
32 29 30 31 3anbi123d 
 |-  ( y = Y -> ( ( X C_ V /\ y C_ V /\ X C_ y ) <-> ( X C_ V /\ Y C_ V /\ X C_ Y ) ) )
33 fveq2 
 |-  ( y = Y -> ( ._|_ ` y ) = ( ._|_ ` Y ) )
34 33 sseq1d 
 |-  ( y = Y -> ( ( ._|_ ` y ) C_ ( ._|_ ` X ) <-> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) )
35 32 34 imbi12d 
 |-  ( y = Y -> ( ( ( X C_ V /\ y C_ V /\ X C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` X ) ) <-> ( ( X C_ V /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) ) )
36 28 35 sylan9bb 
 |-  ( ( x = X /\ y = Y ) -> ( ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) <-> ( ( X C_ V /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) ) )
37 36 spc2gv 
 |-  ( ( X e. ~P V /\ Y e. ~P V ) -> ( A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) -> ( ( X C_ V /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) ) )
38 19 21 37 syl2anc 
 |-  ( ph -> ( A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) -> ( ( X C_ V /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) ) )
39 16 38 mpid 
 |-  ( ph -> ( A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) )
40 15 39 syl5 
 |-  ( ph -> ( ( ._|_ : ~P V --> ( LSubSp ` W ) /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) )
41 14 40 mpd 
 |-  ( ph -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) )