Description: A member of domain of the partial isomorphism A is a lattice element. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | diadmcl.b | |- B = ( Base ` K ) |
|
diadmcl.h | |- H = ( LHyp ` K ) |
||
diadmcl.i | |- I = ( ( DIsoA ` K ) ` W ) |
||
Assertion | diadmclN | |- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X e. B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | diadmcl.b | |- B = ( Base ` K ) |
|
2 | diadmcl.h | |- H = ( LHyp ` K ) |
|
3 | diadmcl.i | |- I = ( ( DIsoA ` K ) ` W ) |
|
4 | eqid | |- ( le ` K ) = ( le ` K ) |
|
5 | 1 4 2 3 | diaeldm | |- ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> ( X e. B /\ X ( le ` K ) W ) ) ) |
6 | 5 | simprbda | |- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X e. B ) |