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 ) )