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

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