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