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	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \to (A, B) \cap (C, D) = (if (A \leq C, C, A), if (B \leq D, B, D))$

Step	Hyp	Ref	Expression
1		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
2		xrmaxlt	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land z \in ℝ^{*}) \to (if (A \leq C, C, A) < z \leftrightarrow (A < z \land C < z))$
3		xrltmin	$⊢ (z \in ℝ^{} \land B \in ℝ^{} \land D \in ℝ^{*}) \to (z < if (B \leq D, B, D) \leftrightarrow (z < B \land z < D))$
4	1 2 3	ixxin	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \to (A, B) \cap (C, D) = (if (A \leq C, C, A), if (B \leq D, B, D))$

Metamath Proof Explorer