clatlem

Description: Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	clatlem.b	$⊢ B = {Base}_{K}$
	clatlem.u	$⊢ U = lub (K)$
	clatlem.g	$⊢ G = glb (K)$
Assertion	clatlem	$⊢ (K \in CLat \land S \subseteq B) \to (U (S) \in B \land G (S) \in B)$

Step	Hyp	Ref	Expression
1		clatlem.b	$⊢ B = {Base}_{K}$
2		clatlem.u	$⊢ U = lub (K)$
3		clatlem.g	$⊢ G = glb (K)$
4		simpl	$⊢ (K \in CLat \land S \subseteq B) \to K \in CLat$
5	1	fvexi	$⊢ B \in V$
6	5	elpw2	$⊢ S \in 𝒫 B \leftrightarrow S \subseteq B$
7	6	bilanri	$⊢ (K \in CLat \land S \subseteq B) \to S \in 𝒫 B$
8	1 2 3	isclat	$⊢ K \in CLat \leftrightarrow (K \in Poset \land (dom U = 𝒫 B \land dom G = 𝒫 B))$
9	8	birani	$⊢ (K \in CLat \land S \subseteq B) \to (K \in Poset \land (dom U = 𝒫 B \land dom G = 𝒫 B))$
10	9	simprld	$⊢ (K \in CLat \land S \subseteq B) \to dom U = 𝒫 B$
11	7 10	eleqtrrd	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom U$
12	1 2 4 11	lubcl	$⊢ (K \in CLat \land S \subseteq B) \to U (S) \in B$
13	9	simprrd	$⊢ (K \in CLat \land S \subseteq B) \to dom G = 𝒫 B$
14	7 13	eleqtrrd	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom G$
15	1 3 4 14	glbcl	$⊢ (K \in CLat \land S \subseteq B) \to G (S) \in B$
16	12 15	jca	$⊢ (K \in CLat \land S \subseteq B) \to (U (S) \in B \land G (S) \in B)$

Metamath Proof Explorer