clatl

Description: A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011) TODO: use eqrelrdv2 to shorten proof and eliminate joindmss and meetdmss ?

		Ref	Expression
	Assertion	clatl	$⊢ K \in CLat \to K \in Lat$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{K} = {Base}_{K}$
2		eqid	$⊢ join (K) = join (K)$
3		simpl	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to K \in Poset$
4	1 2 3	joindmss	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to dom join (K) \subseteq {Base}_{K} \times {Base}_{K}$
5		relxp	$⊢ Rel ({Base}_{K} \times {Base}_{K})$
6	5	a1i	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to Rel ({Base}_{K} \times {Base}_{K})$
7		opelxp	$⊢ ⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \leftrightarrow (x \in {Base}_{K} \land y \in {Base}_{K})$
8		vex	$⊢ x \in V$
9		vex	$⊢ y \in V$
10	8 9	prss	$⊢ (x \in {Base}_{K} \land y \in {Base}_{K}) \leftrightarrow \{x, y\} \subseteq {Base}_{K}$
11	7 10	sylbb	$⊢ ⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to \{x, y\} \subseteq {Base}_{K}$
12		prex	$⊢ \{x, y\} \in V$
13	12	elpw	$⊢ \{x, y\} \in 𝒫 {Base}_{K} \leftrightarrow \{x, y\} \subseteq {Base}_{K}$
14	11 13	sylibr	$⊢ ⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to \{x, y\} \in 𝒫 {Base}_{K}$
15		eleq2	$⊢ dom lub (K) = 𝒫 {Base}_{K} \to (\{x, y\} \in dom lub (K) \leftrightarrow \{x, y\} \in 𝒫 {Base}_{K})$
16	14 15	imbitrrid	$⊢ dom lub (K) = 𝒫 {Base}_{K} \to (⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to \{x, y\} \in dom lub (K))$
17	16	adantl	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to (⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to \{x, y\} \in dom lub (K))$
18		eqid	$⊢ lub (K) = lub (K)$
19	8	a1i	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to x \in V$
20	9	a1i	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to y \in V$
21	18 2 3 19 20	joindef	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to (⟨x, y⟩ \in dom join (K) \leftrightarrow \{x, y\} \in dom lub (K))$
22	17 21	sylibrd	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to (⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to ⟨x, y⟩ \in dom join (K))$
23	6 22	relssdv	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to {Base}_{K} \times {Base}_{K} \subseteq dom join (K)$
24	4 23	eqssd	$⊢ (K \in Poset \land dom lub (K) = 𝒫 {Base}_{K}) \to dom join (K) = {Base}_{K} \times {Base}_{K}$
25	24	ex	$⊢ K \in Poset \to (dom lub (K) = 𝒫 {Base}_{K} \to dom join (K) = {Base}_{K} \times {Base}_{K})$
26		eqid	$⊢ meet (K) = meet (K)$
27		simpl	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to K \in Poset$
28	1 26 27	meetdmss	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to dom meet (K) \subseteq {Base}_{K} \times {Base}_{K}$
29	5	a1i	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to Rel ({Base}_{K} \times {Base}_{K})$
30		eleq2	$⊢ dom glb (K) = 𝒫 {Base}_{K} \to (\{x, y\} \in dom glb (K) \leftrightarrow \{x, y\} \in 𝒫 {Base}_{K})$
31	14 30	imbitrrid	$⊢ dom glb (K) = 𝒫 {Base}_{K} \to (⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to \{x, y\} \in dom glb (K))$
32	31	adantl	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to (⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to \{x, y\} \in dom glb (K))$
33		eqid	$⊢ glb (K) = glb (K)$
34	8	a1i	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to x \in V$
35	9	a1i	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to y \in V$
36	33 26 27 34 35	meetdef	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to (⟨x, y⟩ \in dom meet (K) \leftrightarrow \{x, y\} \in dom glb (K))$
37	32 36	sylibrd	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to (⟨x, y⟩ \in ({Base}_{K} \times {Base}_{K}) \to ⟨x, y⟩ \in dom meet (K))$
38	29 37	relssdv	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to {Base}_{K} \times {Base}_{K} \subseteq dom meet (K)$
39	28 38	eqssd	$⊢ (K \in Poset \land dom glb (K) = 𝒫 {Base}_{K}) \to dom meet (K) = {Base}_{K} \times {Base}_{K}$
40	39	ex	$⊢ K \in Poset \to (dom glb (K) = 𝒫 {Base}_{K} \to dom meet (K) = {Base}_{K} \times {Base}_{K})$
41	25 40	anim12d	$⊢ K \in Poset \to ((dom lub (K) = 𝒫 {Base}_{K} \land dom glb (K) = 𝒫 {Base}_{K}) \to (dom join (K) = {Base}_{K} \times {Base}_{K} \land dom meet (K) = {Base}_{K} \times {Base}_{K}))$
42	41	imdistani	$⊢ (K \in Poset \land (dom lub (K) = 𝒫 {Base}_{K} \land dom glb (K) = 𝒫 {Base}_{K})) \to (K \in Poset \land (dom join (K) = {Base}_{K} \times {Base}_{K} \land dom meet (K) = {Base}_{K} \times {Base}_{K}))$
43	1 18 33	isclat	$⊢ K \in CLat \leftrightarrow (K \in Poset \land (dom lub (K) = 𝒫 {Base}_{K} \land dom glb (K) = 𝒫 {Base}_{K}))$
44	1 2 26	islat	$⊢ K \in Lat \leftrightarrow (K \in Poset \land (dom join (K) = {Base}_{K} \times {Base}_{K} \land dom meet (K) = {Base}_{K} \times {Base}_{K}))$
45	42 43 44	3imtr4i	$⊢ K \in CLat \to K \in Lat$

Metamath Proof Explorer

Theorem clatl

Proof