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

Metamath Proof Explorer

Theorem clatlem

Description: Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011)

Ref Expression
Hypotheses clatlem.b 
|- B = ( Base ` K )
clatlem.u 
|- U = ( lub ` K )
clatlem.g 
|- G = ( glb ` K )
Assertion clatlem 
|- ( ( K e. CLat /\ S C_ B ) -> ( ( U ` S ) e. B /\ ( G ` S ) e. B ) )

Proof

Step Hyp Ref Expression
1 clatlem.b 
 |-  B = ( Base ` K )
2 clatlem.u 
 |-  U = ( lub ` K )
3 clatlem.g 
 |-  G = ( glb ` K )
4 simpl 
 |-  ( ( K e. CLat /\ S C_ B ) -> K e. CLat )
5 1 fvexi 
 |-  B e. _V
6 5 elpw2 
 |-  ( S e. ~P B <-> S C_ B )
7 6 biimpri 
 |-  ( S C_ B -> S e. ~P B )
8 7 adantl 
 |-  ( ( K e. CLat /\ S C_ B ) -> S e. ~P B )
9 1 2 3 isclat 
 |-  ( K e. CLat <-> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
10 9 biimpi 
 |-  ( K e. CLat -> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
11 10 adantr 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
12 11 simprld 
 |-  ( ( K e. CLat /\ S C_ B ) -> dom U = ~P B )
13 8 12 eleqtrrd 
 |-  ( ( K e. CLat /\ S C_ B ) -> S e. dom U )
14 1 2 4 13 lubcl 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( U ` S ) e. B )
15 11 simprrd 
 |-  ( ( K e. CLat /\ S C_ B ) -> dom G = ~P B )
16 8 15 eleqtrrd 
 |-  ( ( K e. CLat /\ S C_ B ) -> S e. dom G )
17 1 3 4 16 glbcl 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
18 14 17 jca 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( ( U ` S ) e. B /\ ( G ` S ) e. B ) )