This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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