Metamath Proof Explorer

Theorem dihord6b

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

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

Proof

Step	Hyp	Ref	Expression
1		dihord3.b	$⊢ B = {Base}_{K}$
2		dihord3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihord3.h	$⊢ H = LHyp (K)$
4		dihord3.i	$⊢ I = DIsoH (K) (W)$
5		simp2r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to \neg X \underset{˙}{\leq} W$
6		simp3r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \underset{˙}{\leq} W$
7		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in Lat$
9		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \in B$
10		simp3l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \in B$
11		simp1r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to W \in H$
12	1 3	lhpbase	$⊢ W \in H \to W \in B$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to W \in B$
14	1 2	lattr	$⊢ (K \in Lat \land (X \in B \land Y \in B \land W \in B)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} W) \to X \underset{˙}{\leq} W)$
15	8 9 10 13 14	syl13anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} W) \to X \underset{˙}{\leq} W)$
16	6 15	mpan2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \to X \underset{˙}{\leq} W)$
17	5 16	mtod	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to \neg X \underset{˙}{\leq} Y$
18	17	pm2.21d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \to I (X) \subseteq I (Y))$
19	18	imp	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} Y) \to I (X) \subseteq I (Y)$