clatglbcl2

Description: Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018)

	Ref	Expression
Hypotheses	clatglbcl.b	$⊢ B = {Base}_{K}$
	clatglbcl.g	$⊢ G = glb (K)$
Assertion	clatglbcl2	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom G$

Step	Hyp	Ref	Expression
1		clatglbcl.b	$⊢ B = {Base}_{K}$
2		clatglbcl.g	$⊢ G = glb (K)$
3	1	fvexi	$⊢ B \in V$
4	3	elpw2	$⊢ S \in 𝒫 B \leftrightarrow S \subseteq B$
5	4	bilanri	$⊢ (K \in CLat \land S \subseteq B) \to S \in 𝒫 B$
6		eqid	$⊢ lub (K) = lub (K)$
7	1 6 2	isclat	$⊢ K \in CLat \leftrightarrow (K \in Poset \land (dom lub (K) = 𝒫 B \land dom G = 𝒫 B))$
8		simprr	$⊢ (K \in Poset \land (dom lub (K) = 𝒫 B \land dom G = 𝒫 B)) \to dom G = 𝒫 B$
9	7 8	sylbi	$⊢ K \in CLat \to dom G = 𝒫 B$
10	9	adantr	$⊢ (K \in CLat \land S \subseteq B) \to dom G = 𝒫 B$
11	5 10	eleqtrrd	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom G$

Metamath Proof Explorer