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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	diadmle.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	diadmle.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
Assertion	diadmleN	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge X\in \mathrm{dom}I\right)\to X\underset{\dot{}}{\le }W$$

Proof

Step	Hyp	Ref	Expression
1		diadmle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		diadmle.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		diadmle.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 1 2 3	diaeldm	$$⊢\left(K\in V\wedge W\in H\right)\to \left(X\in \mathrm{dom}I\leftrightarrow \left(X\in {\mathrm{Base}}_K\wedge X\underset{\dot{}}{\le }W\right)\right)$$
6	5	simplbda	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge X\in \mathrm{dom}I\right)\to X\underset{\dot{}}{\le }W$$