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