Theorem iccin

Description: Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024)

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

Proof

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