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	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eliooxr	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) )
2		elioore	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → 𝐶 ∈ ℝ )
3	1 2	jca	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ ) )
4		df-3an	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) ↔ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ ) )
5	3 4	sylibr	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) )
6		eliooord	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) )
7	5 6	jca	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
8		rexr	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ^* )
9	8	3anim3i	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) )
10	9	anim1i	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
11		elioo3g	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
12	10 11	sylibr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
13	7 12	impbii	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )