Theorem iooin

Description: Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	iooin	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ioo	⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
2		xrmaxlt	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) < 𝑧 ↔ ( 𝐴 < 𝑧 ∧ 𝐶 < 𝑧 ) ) )
3		xrltmin	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝑧 < if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝑧 < 𝐵 ∧ 𝑧 < 𝐷 ) ) )
4	1 2 3	ixxin	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )