Theorem eliocre

Description: A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	eliocre	|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> C e. RR )

Proof

Step	Hyp	Ref	Expression
1		df-ioc	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
2	1	elixx3g	|- ( C e. ( A (,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C <_ B ) ) )
3	2	biimpi	|- ( C e. ( A (,] B ) -> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C <_ B ) ) )
4	3	simpld	|- ( C e. ( A (,] B ) -> ( A e. RR* /\ B e. RR* /\ C e. RR* ) )
5	4	simp3d	|- ( C e. ( A (,] B ) -> C e. RR* )
6	5	adantl	|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> C e. RR* )
7		simpl	|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> B e. RR )
8		mnfxr	|- -oo e. RR*
9	8	a1i	|- ( C e. ( A (,] B ) -> -oo e. RR* )
10	4	simp1d	|- ( C e. ( A (,] B ) -> A e. RR* )
11		mnfle	|- ( A e. RR* -> -oo <_ A )
12	10 11	syl	|- ( C e. ( A (,] B ) -> -oo <_ A )
13	3	simprd	|- ( C e. ( A (,] B ) -> ( A < C /\ C <_ B ) )
14	13	simpld	|- ( C e. ( A (,] B ) -> A < C )
15	9 10 5 12 14	xrlelttrd	|- ( C e. ( A (,] B ) -> -oo < C )
16	15	adantl	|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> -oo < C )
17	13	simprd	|- ( C e. ( A (,] B ) -> C <_ B )
18	17	adantl	|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> C <_ B )
19		xrre	|- ( ( ( C e. RR* /\ B e. RR ) /\ ( -oo < C /\ C <_ B ) ) -> C e. RR )
20	6 7 16 18 19	syl22anc	|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> C e. RR )