Theorem dihord5a

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

	Ref	Expression
Hypotheses	dihord.b	$$⊢B={\mathrm{Base}}_K$$
	dihord.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihord.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihord.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
Assertion	dihord5a	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\wedge \left(Y\in B\wedge \neg Y\underset{\dot{}}{\le }W\right)\right)\wedge I\left(X\right)\subseteq I\left(Y\right)\right)\to X\underset{\dot{}}{\le }Y$$

Proof

Step	Hyp	Ref	Expression
1		dihord.b	$$⊢B={\mathrm{Base}}_K$$
2		dihord.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihord.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dihord.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
5		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
6		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
7		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
8		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
9		eqid	$$⊢\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)=\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)$$
10	1 2 3 5 6 7 8 9 4	dihord5apre	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\wedge \left(Y\in B\wedge \neg Y\underset{\dot{}}{\le }W\right)\right)\wedge I\left(X\right)\subseteq I\left(Y\right)\right)\to X\underset{\dot{}}{\le }Y$$