This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 )