Metamath Proof Explorer

Theorem infglbb

Description: Bidirectional form of infglb . (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 ) ) )
infglbb.3 
|- ( ph -> B C_ A )
Assertion infglbb 
|- ( ( 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 infglbb.3 
 |-  ( ph -> B C_ A )
4 df-inf 
 |-  inf ( B , A , R ) = sup ( B , A , `' R )
5 4 breq1i 
 |-  ( inf ( B , A , R ) R C <-> sup ( B , A , `' R ) R C )
6 simpr 
 |-  ( ( ph /\ C e. A ) -> C e. A )
7 cnvso 
 |-  ( R Or A <-> `' R Or A )
8 1 7 sylib 
 |-  ( ph -> `' R Or A )
9 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 ) ) )
10 8 9 supcl 
 |-  ( ph -> sup ( B , A , `' R ) e. A )
11 10 adantr 
 |-  ( ( ph /\ C e. A ) -> sup ( B , A , `' R ) e. A )
12 brcnvg 
 |-  ( ( C e. A /\ sup ( B , A , `' R ) e. A ) -> ( C `' R sup ( B , A , `' R ) <-> sup ( B , A , `' R ) R C ) )
13 12 bicomd 
 |-  ( ( C e. A /\ sup ( B , A , `' R ) e. A ) -> ( sup ( B , A , `' R ) R C <-> C `' R sup ( B , A , `' R ) ) )
14 6 11 13 syl2anc 
 |-  ( ( ph /\ C e. A ) -> ( sup ( B , A , `' R ) R C <-> C `' R sup ( B , A , `' R ) ) )
15 8 9 3 suplub2 
 |-  ( ( ph /\ C e. A ) -> ( C `' R sup ( B , A , `' R ) <-> E. z e. B C `' R z ) )
16 vex 
 |-  z e. _V
17 brcnvg 
 |-  ( ( C e. A /\ z e. _V ) -> ( C `' R z <-> z R C ) )
18 6 16 17 sylancl 
 |-  ( ( ph /\ C e. A ) -> ( C `' R z <-> z R C ) )
19 18 rexbidv 
 |-  ( ( ph /\ C e. A ) -> ( E. z e. B C `' R z <-> E. z e. B z R C ) )
20 14 15 19 3bitrd 
 |-  ( ( ph /\ C e. A ) -> ( sup ( B , A , `' R ) R C <-> E. z e. B z R C ) )
21 5 20 syl5bb 
 |-  ( ( ph /\ C e. A ) -> ( inf ( B , A , R ) R C <-> E. z e. B z R C ) )