clatlubcl2

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

	Ref	Expression
Hypotheses	clatlubcl.b	$⊢ B = {Base}_{K}$
	clatlubcl.u	$⊢ U = lub (K)$
Assertion	clatlubcl2	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom U$

Step	Hyp	Ref	Expression
1		clatlubcl.b	$⊢ B = {Base}_{K}$
2		clatlubcl.u	$⊢ U = lub (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	$⊢ glb (K) = glb (K)$
7	1 2 6	isclat	$⊢ K \in CLat \leftrightarrow (K \in Poset \land (dom U = 𝒫 B \land dom glb (K) = 𝒫 B))$
8		simprl	$⊢ (K \in Poset \land (dom U = 𝒫 B \land dom glb (K) = 𝒫 B)) \to dom U = 𝒫 B$
9	7 8	sylbi	$⊢ K \in CLat \to dom U = 𝒫 B$
10	9	adantr	$⊢ (K \in CLat \land S \subseteq B) \to dom U = 𝒫 B$
11	5 10	eleqtrrd	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom U$

Metamath Proof Explorer