Metamath Proof Explorer

Theorem diaord

Description: The partial isomorphism A for a lattice K is order-preserving in the region under co-atom W . Part of Lemma M of Crawley p. 120 line 28. (Contributed by NM, 26-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		dia11.b	$⊢ B = {Base}_{K}$
2		dia11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dia11.h	$⊢ H = LHyp (K)$
4		dia11.i	$⊢ I = DIsoA (K) (W)$
5		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
6		eqid	$⊢ trL (K) (W) = trL (K) (W)$
7	1 2 3 5 6 4	diaval	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\}$
8	7	3adant3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X) = \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\}$
9	1 2 3 5 6 4	diaval	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (Y) = \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} Y\}$
10	9	3adant2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (Y) = \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} Y\}$
11	8 10	sseq12d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\} \subseteq \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} Y\})$
12		ss2rab	$⊢ \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\} \subseteq \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} Y\} \leftrightarrow \forall f \in LTrn (K) (W) (trL (K) (W) (f) \underset{˙}{\leq} X \to trL (K) (W) (f) \underset{˙}{\leq} Y)$
13		eqid	$⊢ Atoms (K) = Atoms (K)$
14	1 2 13 3 5 6	trlord	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \leftrightarrow \forall f \in LTrn (K) (W) (trL (K) (W) (f) \underset{˙}{\leq} X \to trL (K) (W) (f) \underset{˙}{\leq} Y))$
15	12 14	bitr4id	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (\{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\} \subseteq \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} Y\} \leftrightarrow X \underset{˙}{\leq} Y)$
16	11 15	bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$