Theorem diadmleN

Description: A member of domain of the partial isomorphism A is under the fiducial hyperplane. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	diadmle.l	|- .<_ = ( le ` K )
	diadmle.h	|- H = ( LHyp ` K )
	diadmle.i	|- I = ( ( DIsoA ` K ) ` W )
Assertion	diadmleN	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X .<_ W )

Proof

Step	Hyp	Ref	Expression
1		diadmle.l	|- .<_ = ( le ` K )
2		diadmle.h	|- H = ( LHyp ` K )
3		diadmle.i	|- I = ( ( DIsoA ` K ) ` W )
4		eqid	|- ( Base ` K ) = ( Base ` K )
5	4 1 2 3	diaeldm	|- ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> ( X e. ( Base ` K ) /\ X .<_ W ) ) )
6	5	simplbda	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X .<_ W )