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