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 = ( Base ` K )
	isclat.u	|- U = ( lub ` K )
	isclat.g	|- G = ( glb ` K )
Assertion	isclat	|- ( K e. CLat <-> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )

Proof

Step	Hyp	Ref	Expression
1		isclat.b	|- B = ( Base ` K )
2		isclat.u	|- U = ( lub ` K )
3		isclat.g	|- G = ( glb ` K )
4		fveq2	|- ( l = K -> ( lub ` l ) = ( lub ` K ) )
5	4 2	eqtr4di	|- ( l = K -> ( lub ` l ) = U )
6	5	dmeqd	|- ( l = K -> dom ( lub ` l ) = dom U )
7		fveq2	|- ( l = K -> ( Base ` l ) = ( Base ` K ) )
8	7 1	eqtr4di	|- ( l = K -> ( Base ` l ) = B )
9	8	pweqd	|- ( l = K -> ~P ( Base ` l ) = ~P B )
10	6 9	eqeq12d	|- ( l = K -> ( dom ( lub ` l ) = ~P ( Base ` l ) <-> dom U = ~P B ) )
11		fveq2	|- ( l = K -> ( glb ` l ) = ( glb ` K ) )
12	11 3	eqtr4di	|- ( l = K -> ( glb ` l ) = G )
13	12	dmeqd	|- ( l = K -> dom ( glb ` l ) = dom G )
14	13 9	eqeq12d	|- ( l = K -> ( dom ( glb ` l ) = ~P ( Base ` l ) <-> dom G = ~P B ) )
15	10 14	anbi12d	|- ( l = K -> ( ( dom ( lub ` l ) = ~P ( Base ` l ) /\ dom ( glb ` l ) = ~P ( Base ` l ) ) <-> ( dom U = ~P B /\ dom G = ~P B ) ) )
16		df-clat	|- CLat = { l e. Poset | ( dom ( lub ` l ) = ~P ( Base ` l ) /\ dom ( glb ` l ) = ~P ( Base ` l ) ) }
17	15 16	elrab2	|- ( K e. CLat <-> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )