Theorem mapdcnv11N

Description: The converse of the map defined by df-mapd is one-to-one. (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	mapdcnv11N	|- ( ph -> ( ( `' M ` X ) = ( `' M ` Y ) <-> X = 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	1 2 3 4 5	mapdcnvordN	|- ( ph -> ( ( `' M ` X ) C_ ( `' M ` Y ) <-> X C_ Y ) )
7	1 2 3 5 4	mapdcnvordN	|- ( ph -> ( ( `' M ` Y ) C_ ( `' M ` X ) <-> Y C_ X ) )
8	6 7	anbi12d	|- ( ph -> ( ( ( `' M ` X ) C_ ( `' M ` Y ) /\ ( `' M ` Y ) C_ ( `' M ` X ) ) <-> ( X C_ Y /\ Y C_ X ) ) )
9		eqss	|- ( ( `' M ` X ) = ( `' M ` Y ) <-> ( ( `' M ` X ) C_ ( `' M ` Y ) /\ ( `' M ` Y ) C_ ( `' M ` X ) ) )
10		eqss	|- ( X = Y <-> ( X C_ Y /\ Y C_ X ) )
11	8 9 10	3bitr4g	|- ( ph -> ( ( `' M ` X ) = ( `' M ` Y ) <-> X = Y ) )