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	|- ( ph -> A C_ RR* )
	xrssre.2	|- ( ph -> -. +oo e. A )
	xrssre.3	|- ( ph -> -. -oo e. A )
Assertion	xrssre	|- ( ph -> A C_ RR )

Proof

Step	Hyp	Ref	Expression
1		xrssre.1	|- ( ph -> A C_ RR* )
2		xrssre.2	|- ( ph -> -. +oo e. A )
3		xrssre.3	|- ( ph -> -. -oo e. A )
4		ssxr	|- ( A C_ RR* -> ( A C_ RR \/ +oo e. A \/ -oo e. A ) )
5	1 4	syl	|- ( ph -> ( A C_ RR \/ +oo e. A \/ -oo e. A ) )
6		3orass	|- ( ( A C_ RR \/ +oo e. A \/ -oo e. A ) <-> ( A C_ RR \/ ( +oo e. A \/ -oo e. A ) ) )
7	5 6	sylib	|- ( ph -> ( A C_ RR \/ ( +oo e. A \/ -oo e. A ) ) )
8	7	orcomd	|- ( ph -> ( ( +oo e. A \/ -oo e. A ) \/ A C_ RR ) )
9	2 3	jca	|- ( ph -> ( -. +oo e. A /\ -. -oo e. A ) )
10		ioran	|- ( -. ( +oo e. A \/ -oo e. A ) <-> ( -. +oo e. A /\ -. -oo e. A ) )
11	9 10	sylibr	|- ( ph -> -. ( +oo e. A \/ -oo e. A ) )
12		df-or	|- ( ( ( +oo e. A \/ -oo e. A ) \/ A C_ RR ) <-> ( -. ( +oo e. A \/ -oo e. A ) -> A C_ RR ) )
13	12	biimpi	|- ( ( ( +oo e. A \/ -oo e. A ) \/ A C_ RR ) -> ( -. ( +oo e. A \/ -oo e. A ) -> A C_ RR ) )
14	8 11 13	sylc	|- ( ph -> A C_ RR )