Metamath Proof Explorer

Theorem xrinfmexpnf

Description: Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion xrinfmexpnf 
|- ( E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) -> E. x e. RR* ( A. y e. ( A u. { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( A u. { +oo } ) z < y ) ) )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( y e. ( A u. { +oo } ) <-> ( y e. A \/ y e. { +oo } ) )
2 simpr 
 |-  ( ( x e. RR* /\ ( y e. A -> -. y < x ) ) -> ( y e. A -> -. y < x ) )
3 velsn 
 |-  ( y e. { +oo } <-> y = +oo )
4 pnfnlt 
 |-  ( x e. RR* -> -. +oo < x )
5 breq1 
 |-  ( y = +oo -> ( y < x <-> +oo < x ) )
6 5 notbid 
 |-  ( y = +oo -> ( -. y < x <-> -. +oo < x ) )
7 4 6 syl5ibrcom 
 |-  ( x e. RR* -> ( y = +oo -> -. y < x ) )
8 3 7 syl5bi 
 |-  ( x e. RR* -> ( y e. { +oo } -> -. y < x ) )
9 8 adantr 
 |-  ( ( x e. RR* /\ ( y e. A -> -. y < x ) ) -> ( y e. { +oo } -> -. y < x ) )
10 2 9 jaod 
 |-  ( ( x e. RR* /\ ( y e. A -> -. y < x ) ) -> ( ( y e. A \/ y e. { +oo } ) -> -. y < x ) )
11 1 10 syl5bi 
 |-  ( ( x e. RR* /\ ( y e. A -> -. y < x ) ) -> ( y e. ( A u. { +oo } ) -> -. y < x ) )
12 11 ex 
 |-  ( x e. RR* -> ( ( y e. A -> -. y < x ) -> ( y e. ( A u. { +oo } ) -> -. y < x ) ) )
13 12 ralimdv2 
 |-  ( x e. RR* -> ( A. y e. A -. y < x -> A. y e. ( A u. { +oo } ) -. y < x ) )
14 elun1 
 |-  ( z e. A -> z e. ( A u. { +oo } ) )
15 14 anim1i 
 |-  ( ( z e. A /\ z < y ) -> ( z e. ( A u. { +oo } ) /\ z < y ) )
16 15 reximi2 
 |-  ( E. z e. A z < y -> E. z e. ( A u. { +oo } ) z < y )
17 16 imim2i 
 |-  ( ( x < y -> E. z e. A z < y ) -> ( x < y -> E. z e. ( A u. { +oo } ) z < y ) )
18 17 ralimi 
 |-  ( A. y e. RR* ( x < y -> E. z e. A z < y ) -> A. y e. RR* ( x < y -> E. z e. ( A u. { +oo } ) z < y ) )
19 13 18 anim12d1 
 |-  ( x e. RR* -> ( ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) -> ( A. y e. ( A u. { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( A u. { +oo } ) z < y ) ) ) )
20 19 reximia 
 |-  ( E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) -> E. x e. RR* ( A. y e. ( A u. { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( A u. { +oo } ) z < y ) ) )