Theorem isclat

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

	Ref	Expression
Hypotheses	isclat.b	$$⊢B={\mathrm{Base}}_K$$
	isclat.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	isclat.g	$$⊢G=\mathrm{glb}\left(K\right)$$
Assertion	isclat	$$⊢K\in \mathrm{CLat}\leftrightarrow \left(K\in \mathrm{Poset}\wedge \left(\mathrm{dom}U=𝒫B\wedge \mathrm{dom}G=𝒫B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isclat.b	$$⊢B={\mathrm{Base}}_K$$
2		isclat.u	$$⊢U=\mathrm{lub}\left(K\right)$$
3		isclat.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		fveq2	$$⊢l=K\to \mathrm{lub}\left(l\right)=\mathrm{lub}\left(K\right)$$
5	4 2	eqtr4di	$$⊢l=K\to \mathrm{lub}\left(l\right)=U$$
6	5	dmeqd	$$⊢l=K\to \mathrm{dom}\mathrm{lub}\left(l\right)=\mathrm{dom}U$$
7		fveq2	$$⊢l=K\to {\mathrm{Base}}_l={\mathrm{Base}}_K$$
8	7 1	eqtr4di	$$⊢l=K\to {\mathrm{Base}}_l=B$$
9	8	pweqd	$$⊢l=K\to 𝒫{\mathrm{Base}}_l=𝒫B$$
10	6 9	eqeq12d	$$⊢l=K\to \left(\mathrm{dom}\mathrm{lub}\left(l\right)=𝒫{\mathrm{Base}}_l\leftrightarrow \mathrm{dom}U=𝒫B\right)$$
11		fveq2	$$⊢l=K\to \mathrm{glb}\left(l\right)=\mathrm{glb}\left(K\right)$$
12	11 3	eqtr4di	$$⊢l=K\to \mathrm{glb}\left(l\right)=G$$
13	12	dmeqd	$$⊢l=K\to \mathrm{dom}\mathrm{glb}\left(l\right)=\mathrm{dom}G$$
14	13 9	eqeq12d	$$⊢l=K\to \left(\mathrm{dom}\mathrm{glb}\left(l\right)=𝒫{\mathrm{Base}}_l\leftrightarrow \mathrm{dom}G=𝒫B\right)$$
15	10 14	anbi12d	$$⊢l=K\to \left(\left(\mathrm{dom}\mathrm{lub}\left(l\right)=𝒫{\mathrm{Base}}_l\wedge \mathrm{dom}\mathrm{glb}\left(l\right)=𝒫{\mathrm{Base}}_l\right)\leftrightarrow \left(\mathrm{dom}U=𝒫B\wedge \mathrm{dom}G=𝒫B\right)\right)$$
16		df-clat	$$⊢\mathrm{CLat}=\left\{l\in \mathrm{Poset}|\left(\mathrm{dom}\mathrm{lub}\left(l\right)=𝒫{\mathrm{Base}}_l\wedge \mathrm{dom}\mathrm{glb}\left(l\right)=𝒫{\mathrm{Base}}_l\right)\right\}$$
17	15 16	elrab2	$$⊢K\in \mathrm{CLat}\leftrightarrow \left(K\in \mathrm{Poset}\wedge \left(\mathrm{dom}U=𝒫B\wedge \mathrm{dom}G=𝒫B\right)\right)$$