Metamath Proof Explorer

Theorem clatglbss

Description: Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014)

		Ref	Expression
	Hypotheses	clatglb.b	$⊢ B = {Base}_{K}$
		clatglb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		clatglb.g	$⊢ G = glb (K)$
	Assertion	clatglbss	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to G (T) \underset{˙}{\leq} G (S)$

Proof

Step	Hyp	Ref	Expression
1		clatglb.b	$⊢ B = {Base}_{K}$
2		clatglb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		clatglb.g	$⊢ G = glb (K)$
4		simpl1	$⊢ ((K \in CLat \land T \subseteq B \land S \subseteq T) \land y \in S) \to K \in CLat$
5		simpl2	$⊢ ((K \in CLat \land T \subseteq B \land S \subseteq T) \land y \in S) \to T \subseteq B$
6		simp3	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to S \subseteq T$
7	6	sselda	$⊢ ((K \in CLat \land T \subseteq B \land S \subseteq T) \land y \in S) \to y \in T$
8	1 2 3	clatglble	$⊢ (K \in CLat \land T \subseteq B \land y \in T) \to G (T) \underset{˙}{\leq} y$
9	4 5 7 8	syl3anc	$⊢ ((K \in CLat \land T \subseteq B \land S \subseteq T) \land y \in S) \to G (T) \underset{˙}{\leq} y$
10	9	ralrimiva	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to \forall y \in S G (T) \underset{˙}{\leq} y$
11		simp1	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to K \in CLat$
12	1 3	clatglbcl	$⊢ (K \in CLat \land T \subseteq B) \to G (T) \in B$
13	12	3adant3	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to G (T) \in B$
14		sstr	$⊢ (S \subseteq T \land T \subseteq B) \to S \subseteq B$
15	14	ancoms	$⊢ (T \subseteq B \land S \subseteq T) \to S \subseteq B$
16	15	3adant1	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to S \subseteq B$
17	1 2 3	clatleglb	$⊢ (K \in CLat \land G (T) \in B \land S \subseteq B) \to (G (T) \underset{˙}{\leq} G (S) \leftrightarrow \forall y \in S G (T) \underset{˙}{\leq} y)$
18	11 13 16 17	syl3anc	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to (G (T) \underset{˙}{\leq} G (S) \leftrightarrow \forall y \in S G (T) \underset{˙}{\leq} y)$
19	10 18	mpbird	$⊢ (K \in CLat \land T \subseteq B \land S \subseteq T) \to G (T) \underset{˙}{\leq} G (S)$