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

Metamath Proof Explorer

Theorem infxrpnf

Description: Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion infxrpnf 
|- ( A C_ RR* -> inf ( ( A u. { +oo } ) , RR* , < ) = inf ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A C_ RR* -> A C_ RR* )
2 pnfxr 
 |-  +oo e. RR*
3 snssi 
 |-  ( +oo e. RR* -> { +oo } C_ RR* )
4 2 3 ax-mp 
 |-  { +oo } C_ RR*
5 4 a1i 
 |-  ( A C_ RR* -> { +oo } C_ RR* )
6 1 5 unssd 
 |-  ( A C_ RR* -> ( A u. { +oo } ) C_ RR* )
7 6 infxrcld 
 |-  ( A C_ RR* -> inf ( ( A u. { +oo } ) , RR* , < ) e. RR* )
8 infxrcl 
 |-  ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
9 ssun1 
 |-  A C_ ( A u. { +oo } )
10 9 a1i 
 |-  ( A C_ RR* -> A C_ ( A u. { +oo } ) )
11 infxrss 
 |-  ( ( A C_ ( A u. { +oo } ) /\ ( A u. { +oo } ) C_ RR* ) -> inf ( ( A u. { +oo } ) , RR* , < ) <_ inf ( A , RR* , < ) )
12 10 6 11 syl2anc 
 |-  ( A C_ RR* -> inf ( ( A u. { +oo } ) , RR* , < ) <_ inf ( A , RR* , < ) )
13 infeq1 
 |-  ( A = (/) -> inf ( A , RR* , < ) = inf ( (/) , RR* , < ) )
14 xrinf0 
 |-  inf ( (/) , RR* , < ) = +oo
15 14 2 eqeltri 
 |-  inf ( (/) , RR* , < ) e. RR*
16 15 a1i 
 |-  ( A = (/) -> inf ( (/) , RR* , < ) e. RR* )
17 13 16 eqeltrd 
 |-  ( A = (/) -> inf ( A , RR* , < ) e. RR* )
18 xrltso 
 |-  < Or RR*
19 infsn 
 |-  ( ( < Or RR* /\ +oo e. RR* ) -> inf ( { +oo } , RR* , < ) = +oo )
20 18 2 19 mp2an 
 |-  inf ( { +oo } , RR* , < ) = +oo
21 20 eqcomi 
 |-  +oo = inf ( { +oo } , RR* , < )
22 21 a1i 
 |-  ( A = (/) -> +oo = inf ( { +oo } , RR* , < ) )
23 13 14 eqtrdi 
 |-  ( A = (/) -> inf ( A , RR* , < ) = +oo )
24 uneq1 
 |-  ( A = (/) -> ( A u. { +oo } ) = ( (/) u. { +oo } ) )
25 0un 
 |-  ( (/) u. { +oo } ) = { +oo }
26 25 a1i 
 |-  ( A = (/) -> ( (/) u. { +oo } ) = { +oo } )
27 24 26 eqtrd 
 |-  ( A = (/) -> ( A u. { +oo } ) = { +oo } )
28 27 infeq1d 
 |-  ( A = (/) -> inf ( ( A u. { +oo } ) , RR* , < ) = inf ( { +oo } , RR* , < ) )
29 22 23 28 3eqtr4d 
 |-  ( A = (/) -> inf ( A , RR* , < ) = inf ( ( A u. { +oo } ) , RR* , < ) )
30 17 29 xreqled 
 |-  ( A = (/) -> inf ( A , RR* , < ) <_ inf ( ( A u. { +oo } ) , RR* , < ) )
31 30 adantl 
 |-  ( ( A C_ RR* /\ A = (/) ) -> inf ( A , RR* , < ) <_ inf ( ( A u. { +oo } ) , RR* , < ) )
32 neqne 
 |-  ( -. A = (/) -> A =/= (/) )
33 nfv 
 |-  F/ x ( A C_ RR* /\ A =/= (/) )
34 nfv 
 |-  F/ y ( A C_ RR* /\ A =/= (/) )
35 simpl 
 |-  ( ( A C_ RR* /\ A =/= (/) ) -> A C_ RR* )
36 35 6 syl 
 |-  ( ( A C_ RR* /\ A =/= (/) ) -> ( A u. { +oo } ) C_ RR* )
37 simpr 
 |-  ( ( A C_ RR* /\ x e. A ) -> x e. A )
38 ssel2 
 |-  ( ( A C_ RR* /\ x e. A ) -> x e. RR* )
39 38 xrleidd 
 |-  ( ( A C_ RR* /\ x e. A ) -> x <_ x )
40 breq1 
 |-  ( y = x -> ( y <_ x <-> x <_ x ) )
41 40 rspcev 
 |-  ( ( x e. A /\ x <_ x ) -> E. y e. A y <_ x )
42 37 39 41 syl2anc 
 |-  ( ( A C_ RR* /\ x e. A ) -> E. y e. A y <_ x )
43 42 ad4ant14 
 |-  ( ( ( ( A C_ RR* /\ A =/= (/) ) /\ x e. ( A u. { +oo } ) ) /\ x e. A ) -> E. y e. A y <_ x )
44 simpll 
 |-  ( ( ( ( A C_ RR* /\ A =/= (/) ) /\ x e. ( A u. { +oo } ) ) /\ -. x e. A ) -> ( A C_ RR* /\ A =/= (/) ) )
45 elunnel1 
 |-  ( ( x e. ( A u. { +oo } ) /\ -. x e. A ) -> x e. { +oo } )
46 elsni 
 |-  ( x e. { +oo } -> x = +oo )
47 45 46 syl 
 |-  ( ( x e. ( A u. { +oo } ) /\ -. x e. A ) -> x = +oo )
48 47 adantll 
 |-  ( ( ( ( A C_ RR* /\ A =/= (/) ) /\ x e. ( A u. { +oo } ) ) /\ -. x e. A ) -> x = +oo )
49 simplr 
 |-  ( ( ( A C_ RR* /\ A =/= (/) ) /\ x = +oo ) -> A =/= (/) )
50 ssel2 
 |-  ( ( A C_ RR* /\ y e. A ) -> y e. RR* )
51 pnfge 
 |-  ( y e. RR* -> y <_ +oo )
52 50 51 syl 
 |-  ( ( A C_ RR* /\ y e. A ) -> y <_ +oo )
53 52 adantlr 
 |-  ( ( ( A C_ RR* /\ x = +oo ) /\ y e. A ) -> y <_ +oo )
54 simplr 
 |-  ( ( ( A C_ RR* /\ x = +oo ) /\ y e. A ) -> x = +oo )
55 53 54 breqtrrd 
 |-  ( ( ( A C_ RR* /\ x = +oo ) /\ y e. A ) -> y <_ x )
56 55 ralrimiva 
 |-  ( ( A C_ RR* /\ x = +oo ) -> A. y e. A y <_ x )
57 56 adantlr 
 |-  ( ( ( A C_ RR* /\ A =/= (/) ) /\ x = +oo ) -> A. y e. A y <_ x )
58 r19.2z 
 |-  ( ( A =/= (/) /\ A. y e. A y <_ x ) -> E. y e. A y <_ x )
59 49 57 58 syl2anc 
 |-  ( ( ( A C_ RR* /\ A =/= (/) ) /\ x = +oo ) -> E. y e. A y <_ x )
60 44 48 59 syl2anc 
 |-  ( ( ( ( A C_ RR* /\ A =/= (/) ) /\ x e. ( A u. { +oo } ) ) /\ -. x e. A ) -> E. y e. A y <_ x )
61 43 60 pm2.61dan 
 |-  ( ( ( A C_ RR* /\ A =/= (/) ) /\ x e. ( A u. { +oo } ) ) -> E. y e. A y <_ x )
62 33 34 35 36 61 infleinf2 
 |-  ( ( A C_ RR* /\ A =/= (/) ) -> inf ( A , RR* , < ) <_ inf ( ( A u. { +oo } ) , RR* , < ) )
63 32 62 sylan2 
 |-  ( ( A C_ RR* /\ -. A = (/) ) -> inf ( A , RR* , < ) <_ inf ( ( A u. { +oo } ) , RR* , < ) )
64 31 63 pm2.61dan 
 |-  ( A C_ RR* -> inf ( A , RR* , < ) <_ inf ( ( A u. { +oo } ) , RR* , < ) )
65 7 8 12 64 xrletrid 
 |-  ( A C_ RR* -> inf ( ( A u. { +oo } ) , RR* , < ) = inf ( A , RR* , < ) )