islat

Description: The predicate "is a lattice". (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	islat.b	$⊢ B = {Base}_{K}$
	islat.j	$⊢ \underset{˙}{\lor} = join (K)$
	islat.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	islat	$⊢ K \in Lat \leftrightarrow (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom \underset{˙}{\land} = B \times B))$

Step	Hyp	Ref	Expression
1		islat.b	$⊢ B = {Base}_{K}$
2		islat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		islat.m	$⊢ \underset{˙}{\land} = meet (K)$
4		fveq2	$⊢ l = K \to join (l) = join (K)$
5	4 2	eqtr4di	$⊢ l = K \to join (l) = \underset{˙}{\lor}$
6	5	dmeqd	$⊢ l = K \to dom join (l) = dom \underset{˙}{\lor}$
7		fveq2	$⊢ l = K \to {Base}_{l} = {Base}_{K}$
8	7 1	eqtr4di	$⊢ l = K \to {Base}_{l} = B$
9	8	sqxpeqd	$⊢ l = K \to {Base}_{l} \times {Base}_{l} = B \times B$
10	6 9	eqeq12d	$⊢ l = K \to (dom join (l) = {Base}_{l} \times {Base}_{l} \leftrightarrow dom \underset{˙}{\lor} = B \times B)$
11		fveq2	$⊢ l = K \to meet (l) = meet (K)$
12	11 3	eqtr4di	$⊢ l = K \to meet (l) = \underset{˙}{\land}$
13	12	dmeqd	$⊢ l = K \to dom meet (l) = dom \underset{˙}{\land}$
14	13 9	eqeq12d	$⊢ l = K \to (dom meet (l) = {Base}_{l} \times {Base}_{l} \leftrightarrow dom \underset{˙}{\land} = B \times B)$
15	10 14	anbi12d	$⊢ l = K \to ((dom join (l) = {Base}_{l} \times {Base}_{l} \land dom meet (l) = {Base}_{l} \times {Base}_{l}) \leftrightarrow (dom \underset{˙}{\lor} = B \times B \land dom \underset{˙}{\land} = B \times B))$
16		df-lat	$⊢ Lat = \{l \in Poset \| (dom join (l) = {Base}_{l} \times {Base}_{l} \land dom meet (l) = {Base}_{l} \times {Base}_{l})\}$
17	15 16	elrab2	$⊢ K \in Lat \leftrightarrow (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom \underset{˙}{\land} = B \times B))$

Metamath Proof Explorer