Metamath Proof Explorer


Theorem pclssN

Description: Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclss.a
|- A = ( Atoms ` K )
pclss.c
|- U = ( PCl ` K )
Assertion pclssN
|- ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> ( U ` X ) C_ ( U ` Y ) )

Proof

Step Hyp Ref Expression
1 pclss.a
 |-  A = ( Atoms ` K )
2 pclss.c
 |-  U = ( PCl ` K )
3 sstr2
 |-  ( X C_ Y -> ( Y C_ y -> X C_ y ) )
4 3 3ad2ant2
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> ( Y C_ y -> X C_ y ) )
5 4 adantr
 |-  ( ( ( K e. V /\ X C_ Y /\ Y C_ A ) /\ y e. ( PSubSp ` K ) ) -> ( Y C_ y -> X C_ y ) )
6 5 ss2rabdv
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> { y e. ( PSubSp ` K ) | Y C_ y } C_ { y e. ( PSubSp ` K ) | X C_ y } )
7 intss
 |-  ( { y e. ( PSubSp ` K ) | Y C_ y } C_ { y e. ( PSubSp ` K ) | X C_ y } -> |^| { y e. ( PSubSp ` K ) | X C_ y } C_ |^| { y e. ( PSubSp ` K ) | Y C_ y } )
8 6 7 syl
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> |^| { y e. ( PSubSp ` K ) | X C_ y } C_ |^| { y e. ( PSubSp ` K ) | Y C_ y } )
9 simp1
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> K e. V )
10 sstr
 |-  ( ( X C_ Y /\ Y C_ A ) -> X C_ A )
11 10 3adant1
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> X C_ A )
12 eqid
 |-  ( PSubSp ` K ) = ( PSubSp ` K )
13 1 12 2 pclvalN
 |-  ( ( K e. V /\ X C_ A ) -> ( U ` X ) = |^| { y e. ( PSubSp ` K ) | X C_ y } )
14 9 11 13 syl2anc
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> ( U ` X ) = |^| { y e. ( PSubSp ` K ) | X C_ y } )
15 1 12 2 pclvalN
 |-  ( ( K e. V /\ Y C_ A ) -> ( U ` Y ) = |^| { y e. ( PSubSp ` K ) | Y C_ y } )
16 15 3adant2
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> ( U ` Y ) = |^| { y e. ( PSubSp ` K ) | Y C_ y } )
17 8 14 16 3sstr4d
 |-  ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> ( U ` X ) C_ ( U ` Y ) )