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 ( 𝐴 ⊆ ℝ* → inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) = inf ( 𝐴 , ℝ* , < ) )

Proof

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