Theorem dibclN

Description: Closure of partial isomorphism B for a lattice K . (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dibcl.h	|- H = ( LHyp ` K )
	dibcl.i	|- I = ( ( DIsoB ` K ) ` W )
Assertion	dibclN	|- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran I )

Proof

Step	Hyp	Ref	Expression
1		dibcl.h	|- H = ( LHyp ` K )
2		dibcl.i	|- I = ( ( DIsoB ` K ) ` W )
3		eqid	|- ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
4	1 3 2	dibfna	|- ( ( K e. HL /\ W e. H ) -> I Fn dom ( ( DIsoA ` K ) ` W ) )
5		fnfun	|- ( I Fn dom ( ( DIsoA ` K ) ` W ) -> Fun I )
6	4 5	syl	|- ( ( K e. HL /\ W e. H ) -> Fun I )
7		fvelrn	|- ( ( Fun I /\ X e. dom I ) -> ( I ` X ) e. ran I )
8	6 7	sylan	|- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran I )