Metamath Proof Explorer

Theorem clatleglb

Description: Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011)

Ref Expression
Hypotheses clatglb.b 
|- B = ( Base ` K )
clatglb.l 
|- .<_ = ( le ` K )
clatglb.g 
|- G = ( glb ` K )
Assertion clatleglb 
|- ( ( K e. CLat /\ X e. B /\ S C_ B ) -> ( X .<_ ( G ` S ) <-> A. y e. S X .<_ y ) )

Proof

Step Hyp Ref Expression
1 clatglb.b 
 |-  B = ( Base ` K )
2 clatglb.l 
 |-  .<_ = ( le ` K )
3 clatglb.g 
 |-  G = ( glb ` K )
4 1 2 3 clatglble 
 |-  ( ( K e. CLat /\ S C_ B /\ y e. S ) -> ( G ` S ) .<_ y )
5 4 3expa 
 |-  ( ( ( K e. CLat /\ S C_ B ) /\ y e. S ) -> ( G ` S ) .<_ y )
6 5 3adantl2 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> ( G ` S ) .<_ y )
7 simpl1 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> K e. CLat )
8 clatl 
 |-  ( K e. CLat -> K e. Lat )
9 7 8 syl 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> K e. Lat )
10 simpl2 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> X e. B )
11 1 3 clatglbcl 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
12 11 3adant2 
 |-  ( ( K e. CLat /\ X e. B /\ S C_ B ) -> ( G ` S ) e. B )
13 12 adantr 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> ( G ` S ) e. B )
14 ssel 
 |-  ( S C_ B -> ( y e. S -> y e. B ) )
15 14 3ad2ant3 
 |-  ( ( K e. CLat /\ X e. B /\ S C_ B ) -> ( y e. S -> y e. B ) )
16 15 imp 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> y e. B )
17 1 2 lattr 
 |-  ( ( K e. Lat /\ ( X e. B /\ ( G ` S ) e. B /\ y e. B ) ) -> ( ( X .<_ ( G ` S ) /\ ( G ` S ) .<_ y ) -> X .<_ y ) )
18 9 10 13 16 17 syl13anc 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> ( ( X .<_ ( G ` S ) /\ ( G ` S ) .<_ y ) -> X .<_ y ) )
19 6 18 mpan2d 
 |-  ( ( ( K e. CLat /\ X e. B /\ S C_ B ) /\ y e. S ) -> ( X .<_ ( G ` S ) -> X .<_ y ) )
20 19 ralrimdva 
 |-  ( ( K e. CLat /\ X e. B /\ S C_ B ) -> ( X .<_ ( G ` S ) -> A. y e. S X .<_ y ) )
21 1 2 3 clatglb 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( A. y e. S ( G ` S ) .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ ( G ` S ) ) ) )
22 breq1 
 |-  ( z = X -> ( z .<_ y <-> X .<_ y ) )
23 22 ralbidv 
 |-  ( z = X -> ( A. y e. S z .<_ y <-> A. y e. S X .<_ y ) )
24 breq1 
 |-  ( z = X -> ( z .<_ ( G ` S ) <-> X .<_ ( G ` S ) ) )
25 23 24 imbi12d 
 |-  ( z = X -> ( ( A. y e. S z .<_ y -> z .<_ ( G ` S ) ) <-> ( A. y e. S X .<_ y -> X .<_ ( G ` S ) ) ) )
26 25 rspccv 
 |-  ( A. z e. B ( A. y e. S z .<_ y -> z .<_ ( G ` S ) ) -> ( X e. B -> ( A. y e. S X .<_ y -> X .<_ ( G ` S ) ) ) )
27 21 26 simpl2im 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( X e. B -> ( A. y e. S X .<_ y -> X .<_ ( G ` S ) ) ) )
28 27 ex 
 |-  ( K e. CLat -> ( S C_ B -> ( X e. B -> ( A. y e. S X .<_ y -> X .<_ ( G ` S ) ) ) ) )
29 28 com23 
 |-  ( K e. CLat -> ( X e. B -> ( S C_ B -> ( A. y e. S X .<_ y -> X .<_ ( G ` S ) ) ) ) )
30 29 3imp 
 |-  ( ( K e. CLat /\ X e. B /\ S C_ B ) -> ( A. y e. S X .<_ y -> X .<_ ( G ` S ) ) )
31 20 30 impbid 
 |-  ( ( K e. CLat /\ X e. B /\ S C_ B ) -> ( X .<_ ( G ` S ) <-> A. y e. S X .<_ y ) )