Metamath Proof Explorer

Theorem infxrre

Description: The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infxrre ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ* , < ) = inf ( 𝐴 , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → 𝐴 ⊆ ℝ )
2 ressxr ⊢ ℝ ⊆ ℝ*
3 1 2 sstrdi ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → 𝐴 ⊆ ℝ* )
4 infxrcl ⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
5 3 4 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
6 infrecl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ )
7 6 rexrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ* )
8 5 xrleidd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ* , < ) )
9 infxrgelb ⊢ ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) ∈ ℝ* ) → ( inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) )
10 3 5 9 syl2anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) )
11 simp2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → 𝐴 ≠ ∅ )
12 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
13 11 12 sylib ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑧 𝑧 ∈ 𝐴 )
14 5 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
15 1 sselda ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
16 mnfxr ⊢ -∞ ∈ ℝ*
17 16 a1i ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → -∞ ∈ ℝ* )
18 6 mnfltd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → -∞ < inf ( 𝐴 , ℝ , < ) )
19 6 leidd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ , < ) )
20 infregelb ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ inf ( 𝐴 , ℝ , < ) ∈ ℝ ) → ( inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ , < ) ≤ 𝑥 ) )
21 6 20 mpdan ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ , < ) ≤ 𝑥 ) )
22 infxrgelb ⊢ ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ , < ) ∈ ℝ* ) → ( inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ , < ) ≤ 𝑥 ) )
23 3 7 22 syl2anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ , < ) ≤ 𝑥 ) )
24 21 23 bitr4d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ , < ) ↔ inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ* , < ) ) )
25 19 24 mpbid ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ≤ inf ( 𝐴 , ℝ* , < ) )
26 17 7 5 18 25 xrltletrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → -∞ < inf ( 𝐴 , ℝ* , < ) )
27 26 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → -∞ < inf ( 𝐴 , ℝ* , < ) )
28 infxrlb ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑧 ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑧 )
29 3 28 sylan ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑧 )
30 xrre ⊢ ( ( ( inf ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ 𝑧 ∈ ℝ ) ∧ ( -∞ < inf ( 𝐴 , ℝ* , < ) ∧ inf ( 𝐴 , ℝ* , < ) ≤ 𝑧 ) ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ )
31 14 15 27 29 30 syl22anc ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ )
32 13 31 exlimddv ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ )
33 infregelb ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ inf ( 𝐴 , ℝ* , < ) ∈ ℝ ) → ( inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) )
34 32 33 mpdan ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥 ∈ 𝐴 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) )
35 10 34 bitr4d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ* , < ) ↔ inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ , < ) ) )
36 8 35 mpbid ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ , < ) )
37 5 7 36 25 xrletrid ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ* , < ) = inf ( 𝐴 , ℝ , < ) )