Theorem fct2relem

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

	Ref	Expression
Hypotheses	ftc2re.e	$$⊢E=\left(C,D\right)$$
	ftc2re.a	$$⊢\phi \to A\in E$$
	ftc2re.b	$$⊢\phi \to B\in E$$
Assertion	fct2relem	$$⊢\phi \to \left[A,B\right]\subseteq E$$

Proof

Step	Hyp	Ref	Expression
1		ftc2re.e	$$⊢E=\left(C,D\right)$$
2		ftc2re.a	$$⊢\phi \to A\in E$$
3		ftc2re.b	$$⊢\phi \to B\in E$$
4	2 1	eleqtrdi	$$⊢\phi \to A\in \left(C,D\right)$$
5		eliooxr	$$⊢A\in \left(C,D\right)\to \left(C\in {ℝ}^{*}\wedge D\in {ℝ}^{*}\right)$$
6	4 5	syl	$$⊢\phi \to \left(C\in {ℝ}^{*}\wedge D\in {ℝ}^{*}\right)$$
7	6	simpld	$$⊢\phi \to C\in {ℝ}^{*}$$
8	6	simprd	$$⊢\phi \to D\in {ℝ}^{*}$$
9		eliooord	$$⊢A\in \left(C,D\right)\to \left(C<A\wedge A<D\right)$$
10	4 9	syl	$$⊢\phi \to \left(C<A\wedge A<D\right)$$
11	10	simpld	$$⊢\phi \to C<A$$
12	3 1	eleqtrdi	$$⊢\phi \to B\in \left(C,D\right)$$
13		eliooord	$$⊢B\in \left(C,D\right)\to \left(C<B\wedge B<D\right)$$
14	12 13	syl	$$⊢\phi \to \left(C<B\wedge B<D\right)$$
15	14	simprd	$$⊢\phi \to B<D$$
16		iccssioo	$$⊢\left(\left(C\in {ℝ}^{*}\wedge D\in {ℝ}^{*}\right)\wedge \left(C<A\wedge B<D\right)\right)\to \left[A,B\right]\subseteq \left(C,D\right)$$
17	7 8 11 15 16	syl22anc	$$⊢\phi \to \left[A,B\right]\subseteq \left(C,D\right)$$
18	17 1	sseqtrrdi	$$⊢\phi \to \left[A,B\right]\subseteq E$$