This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )