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		inrab2	⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ( ℝ* ∩ ℝ ) ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) }
3		ressxr	⊢ ℝ ⊆ ℝ*
4		sseqin2	⊢ ( ℝ ⊆ ℝ* ↔ ( ℝ* ∩ ℝ ) = ℝ )
5	3 4	mpbi	⊢ ( ℝ* ∩ ℝ ) = ℝ
6	5	rabeqi	⊢ { 𝑥 ∈ ( ℝ* ∩ ℝ ) ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) }
7	2 6	eqtri	⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) }
8		elioore	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ )
9	8	ssriv	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
10	1 9	eqsstrrdi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ⊆ ℝ )
11		df-ss	⊢ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ⊆ ℝ ↔ ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
12	10 11	sylib	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } ∩ ℝ ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
13	7 12	syl5reqr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → { 𝑥 ∈ ℝ* ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )
14	1 13	eqtrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = { 𝑥 ∈ ℝ ∣ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) } )