Theorem fct2relem

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

	Ref	Expression
Hypotheses	ftc2re.e	⊢ 𝐸 = ( 𝐶 (,) 𝐷 )
	ftc2re.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
	ftc2re.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
Assertion	fct2relem	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		ftc2re.e	⊢ 𝐸 = ( 𝐶 (,) 𝐷 )
2		ftc2re.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
3		ftc2re.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
4	2 1	eleqtrdi	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐶 (,) 𝐷 ) )
5		eliooxr	⊢ ( 𝐴 ∈ ( 𝐶 (,) 𝐷 ) → ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) )
6	4 5	syl	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) )
7	6	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
8	6	simprd	⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
9		eliooord	⊢ ( 𝐴 ∈ ( 𝐶 (,) 𝐷 ) → ( 𝐶 < 𝐴 ∧ 𝐴 < 𝐷 ) )
10	4 9	syl	⊢ ( 𝜑 → ( 𝐶 < 𝐴 ∧ 𝐴 < 𝐷 ) )
11	10	simpld	⊢ ( 𝜑 → 𝐶 < 𝐴 )
12	3 1	eleqtrdi	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐶 (,) 𝐷 ) )
13		eliooord	⊢ ( 𝐵 ∈ ( 𝐶 (,) 𝐷 ) → ( 𝐶 < 𝐵 ∧ 𝐵 < 𝐷 ) )
14	12 13	syl	⊢ ( 𝜑 → ( 𝐶 < 𝐵 ∧ 𝐵 < 𝐷 ) )
15	14	simprd	⊢ ( 𝜑 → 𝐵 < 𝐷 )
16		iccssioo	⊢ ( ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ∧ ( 𝐶 < 𝐴 ∧ 𝐵 < 𝐷 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐶 (,) 𝐷 ) )
17	7 8 11 15 16	syl22anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐶 (,) 𝐷 ) )
18	17 1	sseqtrrdi	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 )