Metamath Proof Explorer


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=BaseK
isclat.u U=lubK
isclat.g G=glbK
Assertion isclat KCLatKPosetdomU=𝒫BdomG=𝒫B

Proof

Step Hyp Ref Expression
1 isclat.b B=BaseK
2 isclat.u U=lubK
3 isclat.g G=glbK
4 fveq2 l=Klubl=lubK
5 4 2 eqtr4di l=Klubl=U
6 5 dmeqd l=Kdomlubl=domU
7 fveq2 l=KBasel=BaseK
8 7 1 eqtr4di l=KBasel=B
9 8 pweqd l=K𝒫Basel=𝒫B
10 6 9 eqeq12d l=Kdomlubl=𝒫BaseldomU=𝒫B
11 fveq2 l=Kglbl=glbK
12 11 3 eqtr4di l=Kglbl=G
13 12 dmeqd l=Kdomglbl=domG
14 13 9 eqeq12d l=Kdomglbl=𝒫BaseldomG=𝒫B
15 10 14 anbi12d l=Kdomlubl=𝒫Baseldomglbl=𝒫BaseldomU=𝒫BdomG=𝒫B
16 df-clat CLat=lPoset|domlubl=𝒫Baseldomglbl=𝒫Basel
17 15 16 elrab2 KCLatKPosetdomU=𝒫BdomG=𝒫B