This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clatglbcl2

Description: Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018)

Ref Expression
Hypotheses clatglbcl.b 
|- B = ( Base ` K )
clatglbcl.g 
|- G = ( glb ` K )
Assertion clatglbcl2 
|- ( ( K e. CLat /\ S C_ B ) -> S e. dom G )

Proof

Step Hyp Ref Expression
1 clatglbcl.b 
 |-  B = ( Base ` K )
2 clatglbcl.g 
 |-  G = ( glb ` K )
3 1 fvexi 
 |-  B e. _V
4 3 elpw2 
 |-  ( S e. ~P B <-> S C_ B )
5 4 biimpri 
 |-  ( S C_ B -> S e. ~P B )
6 5 adantl 
 |-  ( ( K e. CLat /\ S C_ B ) -> S e. ~P B )
7 eqid 
 |-  ( lub ` K ) = ( lub ` K )
8 1 7 2 isclat 
 |-  ( K e. CLat <-> ( K e. Poset /\ ( dom ( lub ` K ) = ~P B /\ dom G = ~P B ) ) )
9 simprr 
 |-  ( ( K e. Poset /\ ( dom ( lub ` K ) = ~P B /\ dom G = ~P B ) ) -> dom G = ~P B )
10 8 9 sylbi 
 |-  ( K e. CLat -> dom G = ~P B )
11 10 adantr 
 |-  ( ( K e. CLat /\ S C_ B ) -> dom G = ~P B )
12 6 11 eleqtrrd 
 |-  ( ( K e. CLat /\ S C_ B ) -> S e. dom G )