Metamath Proof Explorer


Theorem diadmclN

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 )

Proof

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 )