toslat

		Ref	Expression
	Assertion	toslat	$⊢ K \in Toset \to K \in Lat$

Proof

Step	Hyp	Ref	Expression
1		tospos	$⊢ K \in Toset \to K \in Poset$
2	1	ad2antrr	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land x \leq_{K} y) \to K \in Poset$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4		simplrl	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land x \leq_{K} y) \to x \in {Base}_{K}$
5		simplrr	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land x \leq_{K} y) \to y \in {Base}_{K}$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7		simpr	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land x \leq_{K} y) \to x \leq_{K} y$
8		eqidd	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land x \leq_{K} y) \to \{x, y\} = \{x, y\}$
9		eqid	$⊢ lub (K) = lub (K)$
10	2 3 4 5 6 7 8 9	lubprdm	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land x \leq_{K} y) \to \{x, y\} \in dom lub (K)$
11	1	ad2antrr	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land y \leq_{K} x) \to K \in Poset$
12		simplrr	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land y \leq_{K} x) \to y \in {Base}_{K}$
13		simplrl	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land y \leq_{K} x) \to x \in {Base}_{K}$
14		simpr	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land y \leq_{K} x) \to y \leq_{K} x$
15		prcom	$⊢ \{x, y\} = \{y, x\}$
16	15	a1i	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land y \leq_{K} x) \to \{x, y\} = \{y, x\}$
17	11 3 12 13 6 14 16 9	lubprdm	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land y \leq_{K} x) \to \{x, y\} \in dom lub (K)$
18	3 6	tleile	$⊢ (K \in Toset \land x \in {Base}_{K} \land y \in {Base}_{K}) \to (x \leq_{K} y \lor y \leq_{K} x)$
19	18	3expb	$⊢ (K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to (x \leq_{K} y \lor y \leq_{K} x)$
20	10 17 19	mpjaodan	$⊢ (K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to \{x, y\} \in dom lub (K)$
21	20	ralrimivva	$⊢ K \in Toset \to \forall x \in {Base}_{K} \forall y \in {Base}_{K} \{x, y\} \in dom lub (K)$
22		eqid	$⊢ join (K) = join (K)$
23	3 1 9 22	joindm2	$⊢ K \in Toset \to (dom join (K) = {Base}_{K} \times {Base}_{K} \leftrightarrow \forall x \in {Base}_{K} \forall y \in {Base}_{K} \{x, y\} \in dom lub (K))$
24	21 23	mpbird	$⊢ K \in Toset \to dom join (K) = {Base}_{K} \times {Base}_{K}$
25		eqid	$⊢ glb (K) = glb (K)$
26	2 3 4 5 6 7 8 25	glbprdm	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land x \leq_{K} y) \to \{x, y\} \in dom glb (K)$
27	11 3 12 13 6 14 16 25	glbprdm	$⊢ ((K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \land y \leq_{K} x) \to \{x, y\} \in dom glb (K)$
28	26 27 19	mpjaodan	$⊢ (K \in Toset \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to \{x, y\} \in dom glb (K)$
29	28	ralrimivva	$⊢ K \in Toset \to \forall x \in {Base}_{K} \forall y \in {Base}_{K} \{x, y\} \in dom glb (K)$
30		eqid	$⊢ meet (K) = meet (K)$
31	3 1 25 30	meetdm2	$⊢ K \in Toset \to (dom meet (K) = {Base}_{K} \times {Base}_{K} \leftrightarrow \forall x \in {Base}_{K} \forall y \in {Base}_{K} \{x, y\} \in dom glb (K))$
32	29 31	mpbird	$⊢ K \in Toset \to dom meet (K) = {Base}_{K} \times {Base}_{K}$
33	24 32	jca	$⊢ K \in Toset \to (dom join (K) = {Base}_{K} \times {Base}_{K} \land dom meet (K) = {Base}_{K} \times {Base}_{K})$
34	3 22 30	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}))$
35	1 33 34	sylanbrc	$⊢ K \in Toset \to K \in Lat$

Metamath Proof Explorer

Theorem toslat

Proof