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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
		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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )