Theorem fct2relem

Description: Lemma for ftc2re . (Contributed by Thierry Arnoux, 20-Dec-2021)

	Ref	Expression
Hypotheses	ftc2re.e	|- E = ( C (,) D )
	ftc2re.a	|- ( ph -> A e. E )
	ftc2re.b	|- ( ph -> B e. E )
Assertion	fct2relem	|- ( ph -> ( A [,] B ) C_ E )

Proof

Step	Hyp	Ref	Expression
1		ftc2re.e	|- E = ( C (,) D )
2		ftc2re.a	|- ( ph -> A e. E )
3		ftc2re.b	|- ( ph -> B e. E )
4	2 1	eleqtrdi	|- ( ph -> A e. ( C (,) D ) )
5		eliooxr	|- ( A e. ( C (,) D ) -> ( C e. RR* /\ D e. RR* ) )
6	4 5	syl	|- ( ph -> ( C e. RR* /\ D e. RR* ) )
7	6	simpld	|- ( ph -> C e. RR* )
8	6	simprd	|- ( ph -> D e. RR* )
9		eliooord	|- ( A e. ( C (,) D ) -> ( C < A /\ A < D ) )
10	4 9	syl	|- ( ph -> ( C < A /\ A < D ) )
11	10	simpld	|- ( ph -> C < A )
12	3 1	eleqtrdi	|- ( ph -> B e. ( C (,) D ) )
13		eliooord	|- ( B e. ( C (,) D ) -> ( C < B /\ B < D ) )
14	12 13	syl	|- ( ph -> ( C < B /\ B < D ) )
15	14	simprd	|- ( ph -> B < D )
16		iccssioo	|- ( ( ( C e. RR* /\ D e. RR* ) /\ ( C < A /\ B < D ) ) -> ( A [,] B ) C_ ( C (,) D ) )
17	7 8 11 15 16	syl22anc	|- ( ph -> ( A [,] B ) C_ ( C (,) D ) )
18	17 1	sseqtrrdi	|- ( ph -> ( A [,] B ) C_ E )