dibord

Description: The isomorphism B for a lattice K is order-preserving in the region under co-atom W . (Contributed by NM, 24-Feb-2014)

	Ref	Expression
Hypotheses	dib11.b	$⊢ B = {Base}_{K}$
	dib11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dib11.h	$⊢ H = LHyp (K)$
	dib11.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibord	$⊢ ((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		dib11.b	$⊢ B = {Base}_{K}$
2		dib11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dib11.h	$⊢ H = LHyp (K)$
4		dib11.i	$⊢ I = DIsoB (K) (W)$
5		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
6		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{B})$
7		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
8	1 2 3 5 6 7 4	dibval2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
9	8	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) = DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
10	1 2 3 5 6 7 4	dibval2	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (Y) = DIsoA (K) (W) (Y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
11	10	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) = DIsoA (K) (W) (Y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
12	9 11	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 DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq DIsoA (K) (W) (Y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\})$
13	1 2 3 4	dibn0	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \neq \emptyset$
14	13	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) \neq \emptyset$
15	9 14	eqnetrrd	$⊢ ((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 DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \neq \emptyset$
16		ssxpb	$⊢ DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \neq \emptyset \to (DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq DIsoA (K) (W) (Y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \leftrightarrow (DIsoA (K) (W) (X) \subseteq DIsoA (K) (W) (Y) \land \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}))$
17	15 16	syl	$⊢ ((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 (DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq DIsoA (K) (W) (Y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \leftrightarrow (DIsoA (K) (W) (X) \subseteq DIsoA (K) (W) (Y) \land \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}))$
18		ssid	$⊢ \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
19	18	biantru	$⊢ DIsoA (K) (W) (X) \subseteq DIsoA (K) (W) (Y) \leftrightarrow (DIsoA (K) (W) (X) \subseteq DIsoA (K) (W) (Y) \land \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\})$
20	1 2 3 7	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 (DIsoA (K) (W) (X) \subseteq DIsoA (K) (W) (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
21	19 20	bitr3id	$⊢ ((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 ((DIsoA (K) (W) (X) \subseteq DIsoA (K) (W) (Y) \land \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}) \leftrightarrow X \underset{˙}{\leq} Y)$
22	12 17 21	3bitrd	$⊢ ((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)$

Metamath Proof Explorer

Theorem dibord

Proof