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

Metamath Proof Explorer

Theorem diaord

Description: The partial isomorphism A for a lattice K is order-preserving in the region under co-atom W . Part of Lemma M of Crawley p. 120 line 28. (Contributed by NM, 26-Nov-2013)

Ref Expression
Hypotheses dia11.b 
|- B = ( Base ` K )
dia11.l 
|- .<_ = ( le ` K )
dia11.h 
|- H = ( LHyp ` K )
dia11.i 
|- I = ( ( DIsoA ` K ) ` W )
Assertion diaord 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )

Proof

Step Hyp Ref Expression
1 dia11.b 
 |-  B = ( Base ` K )
2 dia11.l 
 |-  .<_ = ( le ` K )
3 dia11.h 
 |-  H = ( LHyp ` K )
4 dia11.i 
 |-  I = ( ( DIsoA ` K ) ` W )
5 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
6 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
7 1 2 3 5 6 4 diaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } )
8 7 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` X ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } )
9 1 2 3 5 6 4 diaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` Y ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ Y } )
10 9 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` Y ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ Y } )
11 8 10 sseq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } C_ { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ Y } ) )
12 ss2rab 
 |-  ( { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } C_ { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ Y } <-> A. f e. ( ( LTrn ` K ) ` W ) ( ( ( ( trL ` K ) ` W ) ` f ) .<_ X -> ( ( ( trL ` K ) ` W ) ` f ) .<_ Y ) )
13 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
14 1 2 13 3 5 6 trlord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X .<_ Y <-> A. f e. ( ( LTrn ` K ) ` W ) ( ( ( ( trL ` K ) ` W ) ` f ) .<_ X -> ( ( ( trL ` K ) ` W ) ` f ) .<_ Y ) ) )
15 12 14 bitr4id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } C_ { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ Y } <-> X .<_ Y ) )
16 11 15 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )