Theorem diacnvclN

Description: Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dia1o.h	|- H = ( LHyp ` K )
	dia1o.i	|- I = ( ( DIsoA ` K ) ` W )
Assertion	diacnvclN	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. dom I )

Proof

Step	Hyp	Ref	Expression
1		dia1o.h	|- H = ( LHyp ` K )
2		dia1o.i	|- I = ( ( DIsoA ` K ) ` W )
3	1 2	diaf11N	|- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
4		f1ocnvdm	|- ( ( I : dom I -1-1-onto-> ran I /\ X e. ran I ) -> ( `' I ` X ) e. dom I )
5	3 4	sylan	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. dom I )