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

Proof

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