Theorem iocborel

Description: A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	iocborel.a	|- ( ph -> A e. RR* )
	iocborel.c	|- ( ph -> C e. RR )
	iocborel.t	|- J = ( topGen ` ran (,) )
	iocborel.b	|- B = ( SalGen ` J )
Assertion	iocborel	|- ( ph -> ( A (,] C ) e. B )

Proof

Step	Hyp	Ref	Expression
1		iocborel.a	|- ( ph -> A e. RR* )
2		iocborel.c	|- ( ph -> C e. RR )
3		iocborel.t	|- J = ( topGen ` ran (,) )
4		iocborel.b	|- B = ( SalGen ` J )
5	1 2	iooiinioc	|- ( ph -> |^|_ n e. NN ( A (,) ( C + ( 1 / n ) ) ) = ( A (,] C ) )
6	5	eqcomd	|- ( ph -> ( A (,] C ) = |^|_ n e. NN ( A (,) ( C + ( 1 / n ) ) ) )
7	3 4	bor1sal	|- B e. SAlg
8	7	a1i	|- ( T. -> B e. SAlg )
9		nnct	|- NN ~<_ _om
10	9	a1i	|- ( T. -> NN ~<_ _om )
11		nnn0	|- NN =/= (/)
12	11	a1i	|- ( T. -> NN =/= (/) )
13	3 4	iooborel	|- ( A (,) ( C + ( 1 / n ) ) ) e. B
14	13	a1i	|- ( ( T. /\ n e. NN ) -> ( A (,) ( C + ( 1 / n ) ) ) e. B )
15	8 10 12 14	saliincl	|- ( T. -> |^|_ n e. NN ( A (,) ( C + ( 1 / n ) ) ) e. B )
16	15	mptru	|- |^|_ n e. NN ( A (,) ( C + ( 1 / n ) ) ) e. B
17	16	a1i	|- ( ph -> |^|_ n e. NN ( A (,) ( C + ( 1 / n ) ) ) e. B )
18	6 17	eqeltrd	|- ( ph -> ( A (,] C ) e. B )