Metamath Proof Explorer

Theorem inflb

Description: An infimum is a lower bound. See also infcl and 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 ) ) )
Assertion inflb 
|- ( ph -> ( C e. B -> -. C R inf ( B , A , R ) ) )

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 cnvso 
 |-  ( R Or A <-> `' R Or A )
4 1 3 sylib 
 |-  ( ph -> `' R Or A )
5 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 ) ) )
6 4 5 supub 
 |-  ( ph -> ( C e. B -> -. sup ( B , A , `' R ) `' R C ) )
7 6 imp 
 |-  ( ( ph /\ C e. B ) -> -. sup ( B , A , `' R ) `' R C )
8 df-inf 
 |-  inf ( B , A , R ) = sup ( B , A , `' R )
9 8 a1i 
 |-  ( ( ph /\ C e. B ) -> inf ( B , A , R ) = sup ( B , A , `' R ) )
10 9 breq2d 
 |-  ( ( ph /\ C e. B ) -> ( C R inf ( B , A , R ) <-> C R sup ( B , A , `' R ) ) )
11 4 5 supcl 
 |-  ( ph -> sup ( B , A , `' R ) e. A )
12 brcnvg 
 |-  ( ( sup ( B , A , `' R ) e. A /\ C e. B ) -> ( sup ( B , A , `' R ) `' R C <-> C R sup ( B , A , `' R ) ) )
13 12 bicomd 
 |-  ( ( sup ( B , A , `' R ) e. A /\ C e. B ) -> ( C R sup ( B , A , `' R ) <-> sup ( B , A , `' R ) `' R C ) )
14 11 13 sylan 
 |-  ( ( ph /\ C e. B ) -> ( C R sup ( B , A , `' R ) <-> sup ( B , A , `' R ) `' R C ) )
15 10 14 bitrd 
 |-  ( ( ph /\ C e. B ) -> ( C R inf ( B , A , R ) <-> sup ( B , A , `' R ) `' R C ) )
16 7 15 mtbird 
 |-  ( ( ph /\ C e. B ) -> -. C R inf ( B , A , R ) )
17 16 ex 
 |-  ( ph -> ( C e. B -> -. C R inf ( B , A , R ) ) )