clatleglb

Description: Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011)

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

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	1 2 3	clatglble	$⊢ (K \in CLat \land S \subseteq B \land y \in S) \to G (S) \underset{˙}{\leq} y$
5	4	3expa	$⊢ ((K \in CLat \land S \subseteq B) \land y \in S) \to G (S) \underset{˙}{\leq} y$
6	5	3adantl2	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to G (S) \underset{˙}{\leq} y$
7		simpl1	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to K \in CLat$
8		clatl	$⊢ K \in CLat \to K \in Lat$
9	7 8	syl	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to K \in Lat$
10		simpl2	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to X \in B$
11	1 3	clatglbcl	$⊢ (K \in CLat \land S \subseteq B) \to G (S) \in B$
12	11	3adant2	$⊢ (K \in CLat \land X \in B \land S \subseteq B) \to G (S) \in B$
13	12	adantr	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to G (S) \in B$
14		ssel	$⊢ S \subseteq B \to (y \in S \to y \in B)$
15	14	3ad2ant3	$⊢ (K \in CLat \land X \in B \land S \subseteq B) \to (y \in S \to y \in B)$
16	15	imp	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to y \in B$
17	1 2	lattr	$⊢ (K \in Lat \land (X \in B \land G (S) \in B \land y \in B)) \to ((X \underset{˙}{\leq} G (S) \land G (S) \underset{˙}{\leq} y) \to X \underset{˙}{\leq} y)$
18	9 10 13 16 17	syl13anc	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to ((X \underset{˙}{\leq} G (S) \land G (S) \underset{˙}{\leq} y) \to X \underset{˙}{\leq} y)$
19	6 18	mpan2d	$⊢ ((K \in CLat \land X \in B \land S \subseteq B) \land y \in S) \to (X \underset{˙}{\leq} G (S) \to X \underset{˙}{\leq} y)$
20	19	ralrimdva	$⊢ (K \in CLat \land X \in B \land S \subseteq B) \to (X \underset{˙}{\leq} G (S) \to \forall y \in S X \underset{˙}{\leq} y)$
21	1 2 3	clatglb	$⊢ (K \in CLat \land S \subseteq B) \to (\forall y \in S G (S) \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} G (S)))$
22		breq1	$⊢ z = X \to (z \underset{˙}{\leq} y \leftrightarrow X \underset{˙}{\leq} y)$
23	22	ralbidv	$⊢ z = X \to (\forall y \in S z \underset{˙}{\leq} y \leftrightarrow \forall y \in S X \underset{˙}{\leq} y)$
24		breq1	$⊢ z = X \to (z \underset{˙}{\leq} G (S) \leftrightarrow X \underset{˙}{\leq} G (S))$
25	23 24	imbi12d	$⊢ z = X \to ((\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} G (S)) \leftrightarrow (\forall y \in S X \underset{˙}{\leq} y \to X \underset{˙}{\leq} G (S)))$
26	25	rspccv	$⊢ \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} G (S)) \to (X \in B \to (\forall y \in S X \underset{˙}{\leq} y \to X \underset{˙}{\leq} G (S)))$
27	21 26	simpl2im	$⊢ (K \in CLat \land S \subseteq B) \to (X \in B \to (\forall y \in S X \underset{˙}{\leq} y \to X \underset{˙}{\leq} G (S)))$
28	27	ex	$⊢ K \in CLat \to (S \subseteq B \to (X \in B \to (\forall y \in S X \underset{˙}{\leq} y \to X \underset{˙}{\leq} G (S))))$
29	28	com23	$⊢ K \in CLat \to (X \in B \to (S \subseteq B \to (\forall y \in S X \underset{˙}{\leq} y \to X \underset{˙}{\leq} G (S))))$
30	29	3imp	$⊢ (K \in CLat \land X \in B \land S \subseteq B) \to (\forall y \in S X \underset{˙}{\leq} y \to X \underset{˙}{\leq} G (S))$
31	20 30	impbid	$⊢ (K \in CLat \land X \in B \land S \subseteq B) \to (X \underset{˙}{\leq} G (S) \leftrightarrow \forall y \in S X \underset{˙}{\leq} y)$

Metamath Proof Explorer

Theorem clatleglb

Proof