Metamath Proof Explorer

Theorem dfinfre

Description: The infimum of a set of reals A . (Contributed by NM, 9-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion dfinfre 
|- ( A C_ RR -> inf ( A , RR , < ) = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } )

Proof

Step Hyp Ref Expression
1 df-inf 
 |-  inf ( A , RR , < ) = sup ( A , RR , `' < )
2 df-sup 
 |-  sup ( A , RR , `' < ) = U. { x e. RR | ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) }
3 ssel2 
 |-  ( ( A C_ RR /\ y e. A ) -> y e. RR )
4 vex 
 |-  x e. _V
5 vex 
 |-  y e. _V
6 4 5 brcnv 
 |-  ( x `' < y <-> y < x )
7 6 notbii 
 |-  ( -. x `' < y <-> -. y < x )
8 lenlt 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x <_ y <-> -. y < x ) )
9 7 8 bitr4id 
 |-  ( ( x e. RR /\ y e. RR ) -> ( -. x `' < y <-> x <_ y ) )
10 3 9 sylan2 
 |-  ( ( x e. RR /\ ( A C_ RR /\ y e. A ) ) -> ( -. x `' < y <-> x <_ y ) )
11 10 ancoms 
 |-  ( ( ( A C_ RR /\ y e. A ) /\ x e. RR ) -> ( -. x `' < y <-> x <_ y ) )
12 11 an32s 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( -. x `' < y <-> x <_ y ) )
13 12 ralbidva 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A -. x `' < y <-> A. y e. A x <_ y ) )
14 5 4 brcnv 
 |-  ( y `' < x <-> x < y )
15 vex 
 |-  z e. _V
16 5 15 brcnv 
 |-  ( y `' < z <-> z < y )
17 16 rexbii 
 |-  ( E. z e. A y `' < z <-> E. z e. A z < y )
18 14 17 imbi12i 
 |-  ( ( y `' < x -> E. z e. A y `' < z ) <-> ( x < y -> E. z e. A z < y ) )
19 18 ralbii 
 |-  ( A. y e. RR ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. RR ( x < y -> E. z e. A z < y ) )
20 19 a1i 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. RR ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. RR ( x < y -> E. z e. A z < y ) ) )
21 13 20 anbi12d 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) <-> ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) ) )
22 21 rabbidva 
 |-  ( A C_ RR -> { x e. RR | ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) } = { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } )
23 22 unieqd 
 |-  ( A C_ RR -> U. { x e. RR | ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) } = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } )
24 2 23 syl5eq 
 |-  ( A C_ RR -> sup ( A , RR , `' < ) = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } )
25 1 24 syl5eq 
 |-  ( A C_ RR -> inf ( A , RR , < ) = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } )