Metamath Proof Explorer


Theorem eqinf

Description: Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020)

Ref Expression
Hypothesis infexd.1
|- ( ph -> R Or A )
Assertion eqinf
|- ( ph -> ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) -> inf ( B , A , R ) = C ) )

Proof

Step Hyp Ref Expression
1 infexd.1
 |-  ( ph -> R Or A )
2 df-inf
 |-  inf ( B , A , R ) = sup ( B , A , `' R )
3 cnvso
 |-  ( R Or A <-> `' R Or A )
4 1 3 sylib
 |-  ( ph -> `' R Or A )
5 4 eqsup
 |-  ( ph -> ( ( C e. A /\ A. y e. B -. C `' R y /\ A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) -> sup ( B , A , `' R ) = C ) )
6 brcnvg
 |-  ( ( C e. A /\ y e. _V ) -> ( C `' R y <-> y R C ) )
7 6 bicomd
 |-  ( ( C e. A /\ y e. _V ) -> ( y R C <-> C `' R y ) )
8 7 elvd
 |-  ( C e. A -> ( y R C <-> C `' R y ) )
9 8 notbid
 |-  ( C e. A -> ( -. y R C <-> -. C `' R y ) )
10 9 ralbidv
 |-  ( C e. A -> ( A. y e. B -. y R C <-> A. y e. B -. C `' R y ) )
11 vex
 |-  y e. _V
12 brcnvg
 |-  ( ( y e. _V /\ C e. A ) -> ( y `' R C <-> C R y ) )
13 11 12 mpan
 |-  ( C e. A -> ( y `' R C <-> C R y ) )
14 13 bicomd
 |-  ( C e. A -> ( C R y <-> y `' R C ) )
15 vex
 |-  z e. _V
16 11 15 brcnv
 |-  ( y `' R z <-> z R y )
17 16 a1i
 |-  ( C e. A -> ( y `' R z <-> z R y ) )
18 17 bicomd
 |-  ( C e. A -> ( z R y <-> y `' R z ) )
19 18 rexbidv
 |-  ( C e. A -> ( E. z e. B z R y <-> E. z e. B y `' R z ) )
20 14 19 imbi12d
 |-  ( C e. A -> ( ( C R y -> E. z e. B z R y ) <-> ( y `' R C -> E. z e. B y `' R z ) ) )
21 20 ralbidv
 |-  ( C e. A -> ( A. y e. A ( C R y -> E. z e. B z R y ) <-> A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) )
22 10 21 anbi12d
 |-  ( C e. A -> ( ( A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) <-> ( A. y e. B -. C `' R y /\ A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) ) )
23 22 pm5.32i
 |-  ( ( C e. A /\ ( A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) ) <-> ( C e. A /\ ( A. y e. B -. C `' R y /\ A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) ) )
24 3anass
 |-  ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) <-> ( C e. A /\ ( A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) ) )
25 3anass
 |-  ( ( C e. A /\ A. y e. B -. C `' R y /\ A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) <-> ( C e. A /\ ( A. y e. B -. C `' R y /\ A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) ) )
26 23 24 25 3bitr4i
 |-  ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) <-> ( C e. A /\ A. y e. B -. C `' R y /\ A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) )
27 26 biimpi
 |-  ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) -> ( C e. A /\ A. y e. B -. C `' R y /\ A. y e. A ( y `' R C -> E. z e. B y `' R z ) ) )
28 5 27 impel
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) ) -> sup ( B , A , `' R ) = C )
29 2 28 eqtrid
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) ) -> inf ( B , A , R ) = C )
30 29 ex
 |-  ( ph -> ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) -> inf ( B , A , R ) = C ) )