Metamath Proof Explorer

Theorem xrsupexmnf

Description: Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005)

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

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