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

Metamath Proof Explorer

Theorem ressiooinf

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

Ref Expression
Hypotheses ressiooinf.a ⊢ φ → A ⊆ ℝ
ressiooinf.s ⊢ S = inf A ℝ * <
ressiooinf.n ⊢ φ → ¬ S ∈ A
ressiooinf.i ⊢ I = S +∞
Assertion ressiooinf ⊢ φ → A ⊆ I

Proof

Step Hyp Ref Expression
1 ressiooinf.a ⊢ φ → A ⊆ ℝ
2 ressiooinf.s ⊢ S = inf A ℝ * <
3 ressiooinf.n ⊢ φ → ¬ S ∈ A
4 ressiooinf.i ⊢ I = S +∞
5 ressxr ⊢ ℝ ⊆ ℝ *
6 5 a1i ⊢ φ → ℝ ⊆ ℝ *
7 1 6 sstrd ⊢ φ → A ⊆ ℝ *
8 7 adantr ⊢ φ ∧ x ∈ A → A ⊆ ℝ *
9 8 infxrcld ⊢ φ ∧ x ∈ A → inf A ℝ * < ∈ ℝ *
10 2 9 eqeltrid ⊢ φ ∧ x ∈ A → S ∈ ℝ *
11 pnfxr ⊢ +∞ ∈ ℝ *
12 11 a1i ⊢ φ ∧ x ∈ A → +∞ ∈ ℝ *
13 1 adantr ⊢ φ ∧ x ∈ A → A ⊆ ℝ
14 simpr ⊢ φ ∧ x ∈ A → x ∈ A
15 13 14 sseldd ⊢ φ ∧ x ∈ A → x ∈ ℝ
16 7 sselda ⊢ φ ∧ x ∈ A → x ∈ ℝ *
17 infxrlb ⊢ A ⊆ ℝ * ∧ x ∈ A → inf A ℝ * < ≤ x
18 8 14 17 syl2anc ⊢ φ ∧ x ∈ A → inf A ℝ * < ≤ x
19 2 18 eqbrtrid ⊢ φ ∧ x ∈ A → S ≤ x
20 id ⊢ x = S → x = S
21 20 eqcomd ⊢ x = S → S = x
22 21 adantl ⊢ x ∈ A ∧ x = S → S = x
23 simpl ⊢ x ∈ A ∧ x = S → x ∈ A
24 22 23 eqeltrd ⊢ x ∈ A ∧ x = S → S ∈ A
25 24 adantll ⊢ φ ∧ x ∈ A ∧ x = S → S ∈ A
26 3 ad2antrr ⊢ φ ∧ x ∈ A ∧ x = S → ¬ S ∈ A
27 25 26 pm2.65da ⊢ φ ∧ x ∈ A → ¬ x = S
28 27 neqned ⊢ φ ∧ x ∈ A → x ≠ S
29 28 necomd ⊢ φ ∧ x ∈ A → S ≠ x
30 10 16 19 29 xrleneltd ⊢ φ ∧ x ∈ A → S < x
31 15 ltpnfd ⊢ φ ∧ x ∈ A → x < +∞
32 10 12 15 30 31 eliood ⊢ φ ∧ x ∈ A → x ∈ S +∞
33 32 4 eleqtrrdi ⊢ φ ∧ x ∈ A → x ∈ I
34 33 ralrimiva ⊢ φ → ∀ x ∈ A x ∈ I
35 dfss3 ⊢ A ⊆ I ↔ ∀ x ∈ A x ∈ I
36 34 35 sylibr ⊢ φ → A ⊆ I