Metamath Proof Explorer

Theorem supxrre

Description: The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005) (Proof shortened by Mario Carneiro, 7-Sep-2014)

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

Proof

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