ioorinv

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	ioorinv	$⊢ A \in ran (.) \to (.) (F (A)) = A$

Proof

Step	Hyp	Ref	Expression
1		ioorf.1	$⊢ F = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨sup (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
2		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
3		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
4		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (A \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} A = (a, b))$
5	2 3 4	mp2b	$⊢ A \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} A = (a, b)$
6	1	ioorinv2	$⊢ (a, b) \neq \emptyset \to F ((a, b)) = ⟨a, b⟩$
7	6	fveq2d	$⊢ (a, b) \neq \emptyset \to (.) (F ((a, b))) = (.) (⟨a, b⟩)$
8		df-ov	$⊢ (a, b) = (.) (⟨a, b⟩)$
9	7 8	eqtr4di	$⊢ (a, b) \neq \emptyset \to (.) (F ((a, b))) = (a, b)$
10		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
11		neeq1	$⊢ A = (a, b) \to (A \neq \emptyset \leftrightarrow (a, b) \neq \emptyset)$
12	10 11	bitr3id	$⊢ A = (a, b) \to (\neg A = \emptyset \leftrightarrow (a, b) \neq \emptyset)$
13		2fveq3	$⊢ A = (a, b) \to (.) (F (A)) = (.) (F ((a, b)))$
14		id	$⊢ A = (a, b) \to A = (a, b)$
15	13 14	eqeq12d	$⊢ A = (a, b) \to ((.) (F (A)) = A \leftrightarrow (.) (F ((a, b))) = (a, b))$
16	12 15	imbi12d	$⊢ A = (a, b) \to ((\neg A = \emptyset \to (.) (F (A)) = A) \leftrightarrow ((a, b) \neq \emptyset \to (.) (F ((a, b))) = (a, b)))$
17	9 16	mpbiri	$⊢ A = (a, b) \to (\neg A = \emptyset \to (.) (F (A)) = A)$
18	17	a1i	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (A = (a, b) \to (\neg A = \emptyset \to (.) (F (A)) = A))$
19	18	rexlimivv	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} A = (a, b) \to (\neg A = \emptyset \to (.) (F (A)) = A)$
20	5 19	sylbi	$⊢ A \in ran (.) \to (\neg A = \emptyset \to (.) (F (A)) = A)$
21		ioorebas	$⊢ (0, 0) \in ran (.)$
22	1	ioorval	$⊢ (0, 0) \in ran (.) \to F ((0, 0)) = if ((0, 0) = \emptyset, ⟨0, 0⟩, ⟨sup ((0, 0) ℝ^{} <), sup ((0, 0) ℝ^{} <)⟩)$
23	21 22	ax-mp	$⊢ F ((0, 0)) = if ((0, 0) = \emptyset, ⟨0, 0⟩, ⟨sup ((0, 0) ℝ^{} <), sup ((0, 0) ℝ^{} <)⟩)$
24		iooid	$⊢ (0, 0) = \emptyset$
25	24	iftruei	$⊢ if ((0, 0) = \emptyset, ⟨0, 0⟩, ⟨sup ((0, 0) ℝ^{} <), sup ((0, 0) ℝ^{} <)⟩) = ⟨0, 0⟩$
26	23 25	eqtri	$⊢ F ((0, 0)) = ⟨0, 0⟩$
27	26	fveq2i	$⊢ (.) (F ((0, 0))) = (.) (⟨0, 0⟩)$
28		df-ov	$⊢ (0, 0) = (.) (⟨0, 0⟩)$
29	27 28	eqtr4i	$⊢ (.) (F ((0, 0))) = (0, 0)$
30	24	eqeq2i	$⊢ A = (0, 0) \leftrightarrow A = \emptyset$
31	30	biimpri	$⊢ A = \emptyset \to A = (0, 0)$
32	31	fveq2d	$⊢ A = \emptyset \to F (A) = F ((0, 0))$
33	32	fveq2d	$⊢ A = \emptyset \to (.) (F (A)) = (.) (F ((0, 0)))$
34	29 33 31	3eqtr4a	$⊢ A = \emptyset \to (.) (F (A)) = A$
35	20 34	pm2.61d2	$⊢ A \in ran (.) \to (.) (F (A)) = A$

Metamath Proof Explorer

Theorem ioorinv

Proof