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

Metamath Proof Explorer

Theorem elioo4g

Description: Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion elioo4g ⊢ C ∈ A B ↔ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ A < C ∧ C < B

Proof

Step Hyp Ref Expression
1 eliooxr ⊢ C ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ *
2 elioore ⊢ C ∈ A B → C ∈ ℝ
3 1 2 jca ⊢ C ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ
4 df-3an ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ↔ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ
5 3 4 sylibr ⊢ C ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ
6 eliooord ⊢ C ∈ A B → A < C ∧ C < B
7 5 6 jca ⊢ C ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ A < C ∧ C < B
8 rexr ⊢ C ∈ ℝ → C ∈ ℝ *
9 8 3anim3i ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ *
10 9 anim1i ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ A < C ∧ C < B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < C ∧ C < B
11 elioo3g ⊢ C ∈ A B ↔ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < C ∧ C < B
12 10 11 sylibr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ A < C ∧ C < B → C ∈ A B
13 7 12 impbii ⊢ C ∈ A B ↔ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ A < C ∧ C < B