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
|- ( 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 )