Theorem mapdcnvordN

Description: Ordering property of the converse of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdcnvord.h	|- H = ( LHyp ` K )
	mapdcnvord.m	|- M = ( ( mapd ` K ) ` W )
	mapdcnvord.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdcnvord.x	|- ( ph -> X e. ran M )
	mapdcnvord.y	|- ( ph -> Y e. ran M )
Assertion	mapdcnvordN	|- ( ph -> ( ( `' M ` X ) C_ ( `' M ` Y ) <-> X C_ Y ) )

Proof

Step	Hyp	Ref	Expression
1		mapdcnvord.h	|- H = ( LHyp ` K )
2		mapdcnvord.m	|- M = ( ( mapd ` K ) ` W )
3		mapdcnvord.k	|- ( ph -> ( K e. HL /\ W e. H ) )
4		mapdcnvord.x	|- ( ph -> X e. ran M )
5		mapdcnvord.y	|- ( ph -> Y e. ran M )
6		eqid	|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
7		eqid	|- ( LSubSp ` ( ( DVecH ` K ) ` W ) ) = ( LSubSp ` ( ( DVecH ` K ) ` W ) )
8	1 2 6 7 3 4	mapdcnvcl	|- ( ph -> ( `' M ` X ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )
9	1 2 6 7 3 5	mapdcnvcl	|- ( ph -> ( `' M ` Y ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )
10	1 6 7 2 3 8 9	mapdord	|- ( ph -> ( ( M ` ( `' M ` X ) ) C_ ( M ` ( `' M ` Y ) ) <-> ( `' M ` X ) C_ ( `' M ` Y ) ) )
11	1 2 3 4	mapdcnvid2	|- ( ph -> ( M ` ( `' M ` X ) ) = X )
12	1 2 3 5	mapdcnvid2	|- ( ph -> ( M ` ( `' M ` Y ) ) = Y )
13	11 12	sseq12d	|- ( ph -> ( ( M ` ( `' M ` X ) ) C_ ( M ` ( `' M ` Y ) ) <-> X C_ Y ) )
14	10 13	bitr3d	|- ( ph -> ( ( `' M ` X ) C_ ( `' M ` Y ) <-> X C_ Y ) )