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 )