Metamath Proof Explorer

Theorem infglb

Description: An infimum is the greatest lower bound. See also infcl and inflb . (Contributed by AV, 3-Sep-2020)

Ref Expression
Hypotheses infcl.1 
|- ( ph -> R Or A )
infcl.2 
|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Assertion infglb 
|- ( ph -> ( ( C e. A /\ inf ( B , A , R ) R C ) -> E. z e. B z R C ) )

Proof

Step Hyp Ref Expression
1 infcl.1 
 |-  ( ph -> R Or A )
2 infcl.2 
 |-  ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
3 df-inf 
 |-  inf ( B , A , R ) = sup ( B , A , `' R )
4 3 breq1i 
 |-  ( inf ( B , A , R ) R C <-> sup ( B , A , `' R ) R C )
5 simpr 
 |-  ( ( ph /\ C e. A ) -> C e. A )
6 cnvso 
 |-  ( R Or A <-> `' R Or A )
7 1 6 sylib 
 |-  ( ph -> `' R Or A )
8 1 2 infcllem 
 |-  ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
9 7 8 supcl 
 |-  ( ph -> sup ( B , A , `' R ) e. A )
10 9 adantr 
 |-  ( ( ph /\ C e. A ) -> sup ( B , A , `' R ) e. A )
11 brcnvg 
 |-  ( ( C e. A /\ sup ( B , A , `' R ) e. A ) -> ( C `' R sup ( B , A , `' R ) <-> sup ( B , A , `' R ) R C ) )
12 11 bicomd 
 |-  ( ( C e. A /\ sup ( B , A , `' R ) e. A ) -> ( sup ( B , A , `' R ) R C <-> C `' R sup ( B , A , `' R ) ) )
13 5 10 12 syl2anc 
 |-  ( ( ph /\ C e. A ) -> ( sup ( B , A , `' R ) R C <-> C `' R sup ( B , A , `' R ) ) )
14 4 13 bitrid 
 |-  ( ( ph /\ C e. A ) -> ( inf ( B , A , R ) R C <-> C `' R sup ( B , A , `' R ) ) )
15 7 8 suplub 
 |-  ( ph -> ( ( C e. A /\ C `' R sup ( B , A , `' R ) ) -> E. z e. B C `' R z ) )
16 15 expdimp 
 |-  ( ( ph /\ C e. A ) -> ( C `' R sup ( B , A , `' R ) -> E. z e. B C `' R z ) )
17 vex 
 |-  z e. _V
18 brcnvg 
 |-  ( ( C e. A /\ z e. _V ) -> ( C `' R z <-> z R C ) )
19 5 17 18 sylancl 
 |-  ( ( ph /\ C e. A ) -> ( C `' R z <-> z R C ) )
20 19 rexbidv 
 |-  ( ( ph /\ C e. A ) -> ( E. z e. B C `' R z <-> E. z e. B z R C ) )
21 16 20 sylibd 
 |-  ( ( ph /\ C e. A ) -> ( C `' R sup ( B , A , `' R ) -> E. z e. B z R C ) )
22 14 21 sylbid 
 |-  ( ( ph /\ C e. A ) -> ( inf ( B , A , R ) R C -> E. z e. B z R C ) )
23 22 expimpd 
 |-  ( ph -> ( ( C e. A /\ inf ( B , A , R ) R C ) -> E. z e. B z R C ) )