Theorem dihcnvord

Description: Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014)

	Ref	Expression
Hypotheses	dihcnvord.l	|- .<_ = ( le ` K )
	dihcnvord.h	|- H = ( LHyp ` K )
	dihcnvord.i	|- I = ( ( DIsoH ` K ) ` W )
	dihcnvord.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dihcnvord.x	|- ( ph -> X e. ran I )
	dihcnvord.y	|- ( ph -> Y e. ran I )
Assertion	dihcnvord	|- ( ph -> ( ( `' I ` X ) .<_ ( `' I ` Y ) <-> X C_ Y ) )

Proof

Step	Hyp	Ref	Expression
1		dihcnvord.l	|- .<_ = ( le ` K )
2		dihcnvord.h	|- H = ( LHyp ` K )
3		dihcnvord.i	|- I = ( ( DIsoH ` K ) ` W )
4		dihcnvord.k	|- ( ph -> ( K e. HL /\ W e. H ) )
5		dihcnvord.x	|- ( ph -> X e. ran I )
6		dihcnvord.y	|- ( ph -> Y e. ran I )
7		eqid	|- ( Base ` K ) = ( Base ` K )
8	7 2 3	dihcnvcl	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) )
9	4 5 8	syl2anc	|- ( ph -> ( `' I ` X ) e. ( Base ` K ) )
10	7 2 3	dihcnvcl	|- ( ( ( K e. HL /\ W e. H ) /\ Y e. ran I ) -> ( `' I ` Y ) e. ( Base ` K ) )
11	4 6 10	syl2anc	|- ( ph -> ( `' I ` Y ) e. ( Base ` K ) )
12	7 1 2 3	dihord	|- ( ( ( K e. HL /\ W e. H ) /\ ( `' I ` X ) e. ( Base ` K ) /\ ( `' I ` Y ) e. ( Base ` K ) ) -> ( ( I ` ( `' I ` X ) ) C_ ( I ` ( `' I ` Y ) ) <-> ( `' I ` X ) .<_ ( `' I ` Y ) ) )
13	4 9 11 12	syl3anc	|- ( ph -> ( ( I ` ( `' I ` X ) ) C_ ( I ` ( `' I ` Y ) ) <-> ( `' I ` X ) .<_ ( `' I ` Y ) ) )
14	2 3	dihcnvid2	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X )
15	4 5 14	syl2anc	|- ( ph -> ( I ` ( `' I ` X ) ) = X )
16	2 3	dihcnvid2	|- ( ( ( K e. HL /\ W e. H ) /\ Y e. ran I ) -> ( I ` ( `' I ` Y ) ) = Y )
17	4 6 16	syl2anc	|- ( ph -> ( I ` ( `' I ` Y ) ) = Y )
18	15 17	sseq12d	|- ( ph -> ( ( I ` ( `' I ` X ) ) C_ ( I ` ( `' I ` Y ) ) <-> X C_ Y ) )
19	13 18	bitr3d	|- ( ph -> ( ( `' I ` X ) .<_ ( `' I ` Y ) <-> X C_ Y ) )