Metamath Proof Explorer


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 )