Theorem 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={\mathrm{Base}}_K$$
	islat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	islat.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
Assertion	islat	$$⊢K\in \mathrm{Lat}\leftrightarrow \left(K\in \mathrm{Poset}\wedge \left(\mathrm{dom}\underset{\dot{}}{\vee }=B\times B\wedge \mathrm{dom}\underset{\dot{}}{\wedge }=B\times B\right)\right)$$

Proof

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