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	biimpri	$⊢ S \subseteq B \to S \in 𝒫 B$
8	7	adantl	$⊢ (K \in CLat \land S \subseteq B) \to S \in 𝒫 B$
9	1 2 3	isclat	$⊢ K \in CLat \leftrightarrow (K \in Poset \land (dom U = 𝒫 B \land dom G = 𝒫 B))$
10	9	biimpi	$⊢ K \in CLat \to (K \in Poset \land (dom U = 𝒫 B \land dom G = 𝒫 B))$
11	10	adantr	$⊢ (K \in CLat \land S \subseteq B) \to (K \in Poset \land (dom U = 𝒫 B \land dom G = 𝒫 B))$
12	11	simprld	$⊢ (K \in CLat \land S \subseteq B) \to dom U = 𝒫 B$
13	8 12	eleqtrrd	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom U$
14	1 2 4 13	lubcl	$⊢ (K \in CLat \land S \subseteq B) \to U (S) \in B$
15	11	simprrd	$⊢ (K \in CLat \land S \subseteq B) \to dom G = 𝒫 B$
16	8 15	eleqtrrd	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom G$
17	1 3 4 16	glbcl	$⊢ (K \in CLat \land S \subseteq B) \to G (S) \in B$
18	14 17	jca	$⊢ (K \in CLat \land S \subseteq B) \to (U (S) \in B \land G (S) \in B)$

Metamath Proof Explorer