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	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )