Metamath Proof Explorer

Theorem isglbd

Description: Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Hypotheses isglbd.b 
|- B = ( Base ` K )
isglbd.l 
|- .<_ = ( le ` K )
isglbd.g 
|- G = ( glb ` K )
isglbd.1 
|- ( ( ph /\ y e. S ) -> H .<_ y )
isglbd.2 
|- ( ( ph /\ x e. B /\ A. y e. S x .<_ y ) -> x .<_ H )
isglbd.3 
|- ( ph -> K e. CLat )
isglbd.4 
|- ( ph -> S C_ B )
isglbd.5 
|- ( ph -> H e. B )
Assertion isglbd 
|- ( ph -> ( G ` S ) = H )

Proof

Step Hyp Ref Expression
1 isglbd.b 
 |-  B = ( Base ` K )
2 isglbd.l 
 |-  .<_ = ( le ` K )
3 isglbd.g 
 |-  G = ( glb ` K )
4 isglbd.1 
 |-  ( ( ph /\ y e. S ) -> H .<_ y )
5 isglbd.2 
 |-  ( ( ph /\ x e. B /\ A. y e. S x .<_ y ) -> x .<_ H )
6 isglbd.3 
 |-  ( ph -> K e. CLat )
7 isglbd.4 
 |-  ( ph -> S C_ B )
8 isglbd.5 
 |-  ( ph -> H e. B )
9 biid 
 |-  ( ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) <-> ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) )
10 1 2 3 9 6 7 glbval 
 |-  ( ph -> ( G ` S ) = ( iota_ h e. B ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) ) )
11 4 ralrimiva 
 |-  ( ph -> A. y e. S H .<_ y )
12 5 3exp 
 |-  ( ph -> ( x e. B -> ( A. y e. S x .<_ y -> x .<_ H ) ) )
13 12 ralrimiv 
 |-  ( ph -> A. x e. B ( A. y e. S x .<_ y -> x .<_ H ) )
14 1 3 clatglbcl2 
 |-  ( ( K e. CLat /\ S C_ B ) -> S e. dom G )
15 6 7 14 syl2anc 
 |-  ( ph -> S e. dom G )
16 1 2 3 9 6 15 glbeu 
 |-  ( ph -> E! h e. B ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) )
17 breq1 
 |-  ( h = H -> ( h .<_ y <-> H .<_ y ) )
18 17 ralbidv 
 |-  ( h = H -> ( A. y e. S h .<_ y <-> A. y e. S H .<_ y ) )
19 breq2 
 |-  ( h = H -> ( x .<_ h <-> x .<_ H ) )
20 19 imbi2d 
 |-  ( h = H -> ( ( A. y e. S x .<_ y -> x .<_ h ) <-> ( A. y e. S x .<_ y -> x .<_ H ) ) )
21 20 ralbidv 
 |-  ( h = H -> ( A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) <-> A. x e. B ( A. y e. S x .<_ y -> x .<_ H ) ) )
22 18 21 anbi12d 
 |-  ( h = H -> ( ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) <-> ( A. y e. S H .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ H ) ) ) )
23 22 riota2 
 |-  ( ( H e. B /\ E! h e. B ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) ) -> ( ( A. y e. S H .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ H ) ) <-> ( iota_ h e. B ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) ) = H ) )
24 8 16 23 syl2anc 
 |-  ( ph -> ( ( A. y e. S H .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ H ) ) <-> ( iota_ h e. B ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) ) = H ) )
25 11 13 24 mpbi2and 
 |-  ( ph -> ( iota_ h e. B ( A. y e. S h .<_ y /\ A. x e. B ( A. y e. S x .<_ y -> x .<_ h ) ) ) = H )
26 10 25 eqtrd 
 |-  ( ph -> ( G ` S ) = H )