Theorem diaclN

Description: Closure of partial isomorphism A for a lattice K . (Contributed by NM, 4-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dia1o.h	|- H = ( LHyp ` K )
	dia1o.i	|- I = ( ( DIsoA ` K ) ` W )
Assertion	diaclN	|- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran 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		f1ofun	|- ( I : dom I -1-1-onto-> ran I -> Fun I )
5	3 4	syl	|- ( ( K e. HL /\ W e. H ) -> Fun I )
6		fvelrn	|- ( ( Fun I /\ X e. dom I ) -> ( I ` X ) e. ran I )
7	5 6	sylan	|- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran I )