dihord5a

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

	Ref	Expression
Hypotheses	dihord.b	$⊢ B = {Base}_{K}$
	dihord.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihord.h	$⊢ H = LHyp (K)$
	dihord.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihord5a	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \land I (X) \subseteq I (Y)) \to X \underset{˙}{\leq} Y$

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

Metamath Proof Explorer