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

Metamath Proof Explorer

Theorem xrssre

Description: A subset of extended reals that does not contain +oo and -oo is a subset of the reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses xrssre.1 ⊢ φ → A ⊆ ℝ *
xrssre.2 ⊢ φ → ¬ +∞ ∈ A
xrssre.3 ⊢ φ → ¬ −∞ ∈ A
Assertion xrssre ⊢ φ → A ⊆ ℝ

Proof

Step Hyp Ref Expression
1 xrssre.1 ⊢ φ → A ⊆ ℝ *
2 xrssre.2 ⊢ φ → ¬ +∞ ∈ A
3 xrssre.3 ⊢ φ → ¬ −∞ ∈ A
4 ssxr ⊢ A ⊆ ℝ * → A ⊆ ℝ ∨ +∞ ∈ A ∨ −∞ ∈ A
5 1 4 syl ⊢ φ → A ⊆ ℝ ∨ +∞ ∈ A ∨ −∞ ∈ A
6 3orass ⊢ A ⊆ ℝ ∨ +∞ ∈ A ∨ −∞ ∈ A ↔ A ⊆ ℝ ∨ +∞ ∈ A ∨ −∞ ∈ A
7 5 6 sylib ⊢ φ → A ⊆ ℝ ∨ +∞ ∈ A ∨ −∞ ∈ A
8 7 orcomd ⊢ φ → +∞ ∈ A ∨ −∞ ∈ A ∨ A ⊆ ℝ
9 2 3 jca ⊢ φ → ¬ +∞ ∈ A ∧ ¬ −∞ ∈ A
10 ioran ⊢ ¬ +∞ ∈ A ∨ −∞ ∈ A ↔ ¬ +∞ ∈ A ∧ ¬ −∞ ∈ A
11 9 10 sylibr ⊢ φ → ¬ +∞ ∈ A ∨ −∞ ∈ A
12 df-or ⊢ +∞ ∈ A ∨ −∞ ∈ A ∨ A ⊆ ℝ ↔ ¬ +∞ ∈ A ∨ −∞ ∈ A → A ⊆ ℝ
13 12 biimpi ⊢ +∞ ∈ A ∨ −∞ ∈ A ∨ A ⊆ ℝ → ¬ +∞ ∈ A ∨ −∞ ∈ A → A ⊆ ℝ
14 8 11 13 sylc ⊢ φ → A ⊆ ℝ