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 eqtrid
 |-  ( 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 eqtrid
 |-  ( 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 ) ) } )