This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icomnfinre

Description: A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis icomnfinre.1 
|- ( ph -> A e. RR* )
Assertion icomnfinre 
|- ( ph -> ( ( -oo [,) A ) i^i RR ) = ( -oo (,) A ) )

Proof

Step Hyp Ref Expression
1 icomnfinre.1 
 |-  ( ph -> A e. RR* )
2 mnfxr 
 |-  -oo e. RR*
3 2 a1i 
 |-  ( ( ph /\ x e. ( ( -oo [,) A ) i^i RR ) ) -> -oo e. RR* )
4 1 adantr 
 |-  ( ( ph /\ x e. ( ( -oo [,) A ) i^i RR ) ) -> A e. RR* )
5 elinel2 
 |-  ( x e. ( ( -oo [,) A ) i^i RR ) -> x e. RR )
6 5 adantl 
 |-  ( ( ph /\ x e. ( ( -oo [,) A ) i^i RR ) ) -> x e. RR )
7 6 mnfltd 
 |-  ( ( ph /\ x e. ( ( -oo [,) A ) i^i RR ) ) -> -oo < x )
8 elinel1 
 |-  ( x e. ( ( -oo [,) A ) i^i RR ) -> x e. ( -oo [,) A ) )
9 8 adantl 
 |-  ( ( ph /\ x e. ( ( -oo [,) A ) i^i RR ) ) -> x e. ( -oo [,) A ) )
10 3 4 9 icoltubd 
 |-  ( ( ph /\ x e. ( ( -oo [,) A ) i^i RR ) ) -> x < A )
11 3 4 6 7 10 eliood 
 |-  ( ( ph /\ x e. ( ( -oo [,) A ) i^i RR ) ) -> x e. ( -oo (,) A ) )
12 11 ssd 
 |-  ( ph -> ( ( -oo [,) A ) i^i RR ) C_ ( -oo (,) A ) )
13 ioossico 
 |-  ( -oo (,) A ) C_ ( -oo [,) A )
14 ioossre 
 |-  ( -oo (,) A ) C_ RR
15 13 14 ssini 
 |-  ( -oo (,) A ) C_ ( ( -oo [,) A ) i^i RR )
16 15 a1i 
 |-  ( ph -> ( -oo (,) A ) C_ ( ( -oo [,) A ) i^i RR ) )
17 12 16 eqssd 
 |-  ( ph -> ( ( -oo [,) A ) i^i RR ) = ( -oo (,) A ) )