ioorinv2

Description: The function F is an "inverse" of sorts to the open interval function. (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⟩, ⟨sup (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
	Assertion	ioorinv2	$⊢ (A, B) \neq \emptyset \to F ((A, B)) = ⟨A, B⟩$

Proof

Step	Hyp	Ref	Expression
1		ioorf.1	$⊢ F = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨sup (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
2		ioorebas	$⊢ (A, B) \in ran (.)$
3	1	ioorval	$⊢ (A, B) \in ran (.) \to F ((A, B)) = if ((A, B) = \emptyset, ⟨0, 0⟩, ⟨sup ((A, B) ℝ^{} <), sup ((A, B) ℝ^{} <)⟩)$
4	2 3	ax-mp	$⊢ F ((A, B)) = if ((A, B) = \emptyset, ⟨0, 0⟩, ⟨sup ((A, B) ℝ^{} <), sup ((A, B) ℝ^{} <)⟩)$
5		ifnefalse	$⊢ (A, B) \neq \emptyset \to if ((A, B) = \emptyset, ⟨0, 0⟩, ⟨sup ((A, B) ℝ^{} <), sup ((A, B) ℝ^{} <)⟩) = ⟨sup ((A, B) ℝ^{} <), sup ((A, B) ℝ^{} <)⟩$
6		n0	$⊢ (A, B) \neq \emptyset \leftrightarrow \exists x x \in (A, B)$
7		eliooxr	$⊢ x \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{})$
8	7	exlimiv	$⊢ \exists x x \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{})$
9	6 8	sylbi	$⊢ (A, B) \neq \emptyset \to (A \in ℝ^{} \land B \in ℝ^{})$
10	9	simpld	$⊢ (A, B) \neq \emptyset \to A \in ℝ^{*}$
11	9	simprd	$⊢ (A, B) \neq \emptyset \to B \in ℝ^{*}$
12		id	$⊢ (A, B) \neq \emptyset \to (A, B) \neq \emptyset$
13		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
14		idd	$⊢ (w \in ℝ^{} \land B \in ℝ^{}) \to (w < B \to w < B)$
15		xrltle	$⊢ (w \in ℝ^{} \land B \in ℝ^{}) \to (w < B \to w \leq B)$
16		idd	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A < w)$
17		xrltle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A \leq w)$
18	13 14 15 16 17	ixxlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land (A, B) \neq \emptyset) \to sup ((A, B) ℝ^{*} <) = A$
19	10 11 12 18	syl3anc	$⊢ (A, B) \neq \emptyset \to sup ((A, B) ℝ^{*} <) = A$
20	13 14 15 16 17	ixxub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land (A, B) \neq \emptyset) \to sup ((A, B) ℝ^{*} <) = B$
21	10 11 12 20	syl3anc	$⊢ (A, B) \neq \emptyset \to sup ((A, B) ℝ^{*} <) = B$
22	19 21	opeq12d	$⊢ (A, B) \neq \emptyset \to ⟨sup ((A, B) ℝ^{} <), sup ((A, B) ℝ^{} <)⟩ = ⟨A, B⟩$
23	5 22	eqtrd	$⊢ (A, B) \neq \emptyset \to if ((A, B) = \emptyset, ⟨0, 0⟩, ⟨sup ((A, B) ℝ^{} <), sup ((A, B) ℝ^{} <)⟩) = ⟨A, B⟩$
24	4 23	syl5eq	$⊢ (A, B) \neq \emptyset \to F ((A, B)) = ⟨A, B⟩$

Metamath Proof Explorer

Theorem ioorinv2

Proof