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

Metamath Proof Explorer

Theorem ressioosup

Description: If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ressioosup.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
ressioosup.s ⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
ressioosup.n ⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝐴 )
ressioosup.i ⊢ 𝐼 = ( -∞ (,) 𝑆 )
Assertion ressioosup ( 𝜑 → 𝐴 ⊆ 𝐼 )

Proof

Step Hyp Ref Expression
1 ressioosup.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ressioosup.s ⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
3 ressioosup.n ⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝐴 )
4 ressioosup.i ⊢ 𝐼 = ( -∞ (,) 𝑆 )
5 mnfxr ⊢ -∞ ∈ ℝ*
6 5 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -∞ ∈ ℝ* )
7 ressxr ⊢ ℝ ⊆ ℝ*
8 7 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
9 1 8 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ* )
11 10 supxrcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
12 2 11 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ∈ ℝ* )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
15 13 14 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
16 15 mnfltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -∞ < 𝑥 )
17 9 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
18 supxrub ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ* , < ) )
19 10 14 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ* , < ) )
20 2 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 = sup ( 𝐴 , ℝ* , < ) )
21 20 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = 𝑆 )
22 19 21 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ 𝑆 )
23 id ⊢ ( 𝑥 = 𝑆 → 𝑥 = 𝑆 )
24 23 eqcomd ⊢ ( 𝑥 = 𝑆 → 𝑆 = 𝑥 )
25 24 adantl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑆 = 𝑥 )
26 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑥 ∈ 𝐴 )
27 25 26 eqeltrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑆 ∈ 𝐴 )
28 27 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = 𝑆 ) → 𝑆 ∈ 𝐴 )
29 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = 𝑆 ) → ¬ 𝑆 ∈ 𝐴 )
30 28 29 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 = 𝑆 )
31 30 neqned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ 𝑆 )
32 17 12 22 31 xrleneltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 < 𝑆 )
33 6 12 15 16 32 eliood ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( -∞ (,) 𝑆 ) )
34 33 4 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐼 )
35 34 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
36 dfss3 ⊢ ( 𝐴 ⊆ 𝐼 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
37 35 36 sylibr ⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )