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	$⊢ φ \to A \subseteq ℝ^{*}$
		xrssre.2	$⊢ φ \to \neg +∞ \in A$
		xrssre.3	$⊢ φ \to \neg −∞ \in A$
	Assertion	xrssre	$⊢ φ \to A \subseteq ℝ$

Proof

Step	Hyp	Ref	Expression
1		xrssre.1	$⊢ φ \to A \subseteq ℝ^{*}$
2		xrssre.2	$⊢ φ \to \neg +∞ \in A$
3		xrssre.3	$⊢ φ \to \neg −∞ \in A$
4		ssxr	$⊢ A \subseteq ℝ^{*} \to (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A)$
5	1 4	syl	$⊢ φ \to (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A)$
6		3orass	$⊢ (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A) \leftrightarrow (A \subseteq ℝ \lor (+∞ \in A \lor −∞ \in A))$
7	5 6	sylib	$⊢ φ \to (A \subseteq ℝ \lor (+∞ \in A \lor −∞ \in A))$
8	7	orcomd	$⊢ φ \to ((+∞ \in A \lor −∞ \in A) \lor A \subseteq ℝ)$
9	2 3	jca	$⊢ φ \to (\neg +∞ \in A \land \neg −∞ \in A)$
10		ioran	$⊢ \neg (+∞ \in A \lor −∞ \in A) \leftrightarrow (\neg +∞ \in A \land \neg −∞ \in A)$
11	9 10	sylibr	$⊢ φ \to \neg (+∞ \in A \lor −∞ \in A)$
12		df-or	$⊢ ((+∞ \in A \lor −∞ \in A) \lor A \subseteq ℝ) \leftrightarrow (\neg (+∞ \in A \lor −∞ \in A) \to A \subseteq ℝ)$
13	12	biimpi	$⊢ ((+∞ \in A \lor −∞ \in A) \lor A \subseteq ℝ) \to (\neg (+∞ \in A \lor −∞ \in A) \to A \subseteq ℝ)$
14	8 11 13	sylc	$⊢ φ \to A \subseteq ℝ$