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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
	xrssre.2	⊢ ( 𝜑 → ¬ +∞ ∈ 𝐴 )
	xrssre.3	⊢ ( 𝜑 → ¬ -∞ ∈ 𝐴 )
Assertion	xrssre	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )

Proof

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