Metamath Proof Explorer


Theorem infval

Description: Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020)

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

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 supval2
 |-  ( ph -> sup ( B , A , `' R ) = ( iota_ 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 vex
 |-  x e. _V
7 vex
 |-  y e. _V
8 6 7 brcnv
 |-  ( x `' R y <-> y R x )
9 8 a1i
 |-  ( ph -> ( x `' R y <-> y R x ) )
10 9 notbid
 |-  ( ph -> ( -. x `' R y <-> -. y R x ) )
11 10 ralbidv
 |-  ( ph -> ( A. y e. B -. x `' R y <-> A. y e. B -. y R x ) )
12 7 6 brcnv
 |-  ( y `' R x <-> x R y )
13 12 a1i
 |-  ( ph -> ( y `' R x <-> x R y ) )
14 vex
 |-  z e. _V
15 7 14 brcnv
 |-  ( y `' R z <-> z R y )
16 15 a1i
 |-  ( ph -> ( y `' R z <-> z R y ) )
17 16 rexbidv
 |-  ( ph -> ( E. z e. B y `' R z <-> E. z e. B z R y ) )
18 13 17 imbi12d
 |-  ( ph -> ( ( y `' R x -> E. z e. B y `' R z ) <-> ( x R y -> E. z e. B z R y ) ) )
19 18 ralbidv
 |-  ( ph -> ( A. y e. A ( y `' R x -> E. z e. B y `' R z ) <-> A. y e. A ( x R y -> E. z e. B z R y ) ) )
20 11 19 anbi12d
 |-  ( ph -> ( ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) <-> ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
21 20 riotabidv
 |-  ( ph -> ( iota_ x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
22 5 21 eqtrd
 |-  ( ph -> sup ( B , A , `' R ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
23 2 22 eqtrid
 |-  ( ph -> inf ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )