ioorval

Description: Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)

		Ref	Expression
	Hypothesis	ioorf.1	$⊢ F = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
	Assertion	ioorval	$⊢ A \in ran (.) \to F (A) = if (A = \emptyset, ⟨0, 0⟩, ⟨inf (A ℝ^{} <), sup (A ℝ^{} <)⟩)$

Step	Hyp	Ref	Expression
1		ioorf.1	$⊢ F = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
2		eqeq1	$⊢ x = A \to (x = \emptyset \leftrightarrow A = \emptyset)$
3		infeq1	$⊢ x = A \to inf (x ℝ^{} <) = inf (A ℝ^{} <)$
4		supeq1	$⊢ x = A \to sup (x ℝ^{} <) = sup (A ℝ^{} <)$
5	3 4	opeq12d	$⊢ x = A \to ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩ = ⟨inf (A ℝ^{} <), sup (A ℝ^{} <)⟩$
6	2 5	ifbieq2d	$⊢ x = A \to if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩) = if (A = \emptyset, ⟨0, 0⟩, ⟨inf (A ℝ^{} <), sup (A ℝ^{} <)⟩)$
7		opex	$⊢ ⟨0, 0⟩ \in V$
8		opex	$⊢ ⟨inf (A ℝ^{} <), sup (A ℝ^{} <)⟩ \in V$
9	7 8	ifex	$⊢ if (A = \emptyset, ⟨0, 0⟩, ⟨inf (A ℝ^{} <), sup (A ℝ^{} <)⟩) \in V$
10	6 1 9	fvmpt	$⊢ A \in ran (.) \to F (A) = if (A = \emptyset, ⟨0, 0⟩, ⟨inf (A ℝ^{} <), sup (A ℝ^{} <)⟩)$

Metamath Proof Explorer