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 ( 𝐴 , ℝ , < ) )