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 ) |
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 ) |