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

Metamath Proof Explorer

Theorem iooval2

Description: Value of the open interval function. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iooval2 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )

Proof

Step Hyp Ref Expression
1 iooval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
2 elioore ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ )
3 2 ssriv ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
4 1 3 eqsstrrdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ⊆ ℝ )
5 dfss2 ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ⊆ ℝ ↔ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
6 4 5 sylib ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
7 inrab2 ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ( ℝ* ∩ ℝ ) ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) }
8 ressxr ⊢ ℝ ⊆ ℝ*
9 sseqin2 ⊢ ( ℝ ⊆ ℝ* ↔ ( ℝ* ∩ ℝ ) = ℝ )
10 8 9 mpbi ⊢ ( ℝ* ∩ ℝ ) = ℝ
11 10 rabeqi ⊢ { 𝑥 ∈ ( ℝ* ∩ ℝ ) ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) }
12 7 11 eqtri ⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) }
13 6 12 eqtr3di ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
14 1 13 eqtrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )