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 ⊢ E = C D
ftc2re.a ⊢ φ → A ∈ E
ftc2re.b ⊢ φ → B ∈ E
Assertion fct2relem ⊢ φ → A B ⊆ E

Proof

Step Hyp Ref Expression
1 ftc2re.e ⊢ E = C D
2 ftc2re.a ⊢ φ → A ∈ E
3 ftc2re.b ⊢ φ → B ∈ E
4 2 1 eleqtrdi ⊢ φ → A ∈ C D
5 eliooxr ⊢ A ∈ C D → C ∈ ℝ * ∧ D ∈ ℝ *
6 4 5 syl ⊢ φ → C ∈ ℝ * ∧ D ∈ ℝ *
7 6 simpld ⊢ φ → C ∈ ℝ *
8 6 simprd ⊢ φ → D ∈ ℝ *
9 eliooord ⊢ A ∈ C D → C < A ∧ A < D
10 4 9 syl ⊢ φ → C < A ∧ A < D
11 10 simpld ⊢ φ → C < A
12 3 1 eleqtrdi ⊢ φ → B ∈ C D
13 eliooord ⊢ B ∈ C D → C < B ∧ B < D
14 12 13 syl ⊢ φ → C < B ∧ B < D
15 14 simprd ⊢ φ → B < D
16 iccssioo ⊢ C ∈ ℝ * ∧ D ∈ ℝ * ∧ C < A ∧ B < D → A B ⊆ C D
17 7 8 11 15 16 syl22anc ⊢ φ → A B ⊆ C D
18 17 1 sseqtrrdi ⊢ φ → A B ⊆ E