ioorf

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	ioorf	$⊢ F : ran (.) ⟶ \leq \cap (ℝ^{} \times ℝ^{})$

Proof

Step	Hyp	Ref	Expression
1		ioorf.1	$⊢ F = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
2		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
3		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
4		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (x \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} x = (a, b))$
5	2 3 4	mp2b	$⊢ x \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} x = (a, b)$
6		0le0	$⊢ 0 \leq 0$
7		df-br	$⊢ 0 \leq 0 \leftrightarrow ⟨0, 0⟩ \in \leq$
8	6 7	mpbi	$⊢ ⟨0, 0⟩ \in \leq$
9		0xr	$⊢ 0 \in ℝ^{*}$
10		opelxpi	$⊢ (0 \in ℝ^{} \land 0 \in ℝ^{}) \to ⟨0, 0⟩ \in (ℝ^{} \times ℝ^{})$
11	9 9 10	mp2an	$⊢ ⟨0, 0⟩ \in (ℝ^{} \times ℝ^{})$
12	8 11	elini	$⊢ ⟨0, 0⟩ \in (\leq \cap (ℝ^{} \times ℝ^{}))$
13	12	a1i	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land x = \emptyset) \to ⟨0, 0⟩ \in (\leq \cap (ℝ^{} \times ℝ^{}))$
14		simplr	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to x = (a, b)$
15	14	infeq1d	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to inf (x ℝ^{} <) = inf ((a, b) ℝ^{} <)$
16		simplll	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to a \in ℝ^{*}$
17		simpllr	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to b \in ℝ^{*}$
18		simpr	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to \neg x = \emptyset$
19	18	neqned	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to x \neq \emptyset$
20	14 19	eqnetrrd	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to (a, b) \neq \emptyset$
21		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
22		idd	$⊢ (w \in ℝ^{} \land b \in ℝ^{}) \to (w < b \to w < b)$
23		xrltle	$⊢ (w \in ℝ^{} \land b \in ℝ^{}) \to (w < b \to w \leq b)$
24		idd	$⊢ (a \in ℝ^{} \land w \in ℝ^{}) \to (a < w \to a < w)$
25		xrltle	$⊢ (a \in ℝ^{} \land w \in ℝ^{}) \to (a < w \to a \leq w)$
26	21 22 23 24 25	ixxlb	$⊢ (a \in ℝ^{} \land b \in ℝ^{} \land (a, b) \neq \emptyset) \to inf ((a, b) ℝ^{*} <) = a$
27	16 17 20 26	syl3anc	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to inf ((a, b) ℝ^{*} <) = a$
28	15 27	eqtrd	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to inf (x ℝ^{*} <) = a$
29	14	supeq1d	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to sup (x ℝ^{} <) = sup ((a, b) ℝ^{} <)$
30	21 22 23 24 25	ixxub	$⊢ (a \in ℝ^{} \land b \in ℝ^{} \land (a, b) \neq \emptyset) \to sup ((a, b) ℝ^{*} <) = b$
31	16 17 20 30	syl3anc	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to sup ((a, b) ℝ^{*} <) = b$
32	29 31	eqtrd	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to sup (x ℝ^{*} <) = b$
33	28 32	opeq12d	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩ = ⟨a, b⟩$
34		ioon0	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to ((a, b) \neq \emptyset \leftrightarrow a < b)$
35	34	ad2antrr	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to ((a, b) \neq \emptyset \leftrightarrow a < b)$
36	20 35	mpbid	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to a < b$
37		xrltle	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (a < b \to a \leq b)$
38	37	ad2antrr	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to (a < b \to a \leq b)$
39	36 38	mpd	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to a \leq b$
40		df-br	$⊢ a \leq b \leftrightarrow ⟨a, b⟩ \in \leq$
41	39 40	sylib	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to ⟨a, b⟩ \in \leq$
42		opelxpi	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to ⟨a, b⟩ \in (ℝ^{} \times ℝ^{})$
43	42	ad2antrr	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to ⟨a, b⟩ \in (ℝ^{} \times ℝ^{})$
44	41 43	elind	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to ⟨a, b⟩ \in (\leq \cap (ℝ^{} \times ℝ^{}))$
45	33 44	eqeltrd	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \land \neg x = \emptyset) \to ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩ \in (\leq \cap (ℝ^{} \times ℝ^{}))$
46	13 45	ifclda	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land x = (a, b)) \to if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩) \in (\leq \cap (ℝ^{} \times ℝ^{}))$
47	46	ex	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (x = (a, b) \to if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩) \in (\leq \cap (ℝ^{} \times ℝ^{})))$
48	47	rexlimivv	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} x = (a, b) \to if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩) \in (\leq \cap (ℝ^{} \times ℝ^{}))$
49	5 48	sylbi	$⊢ x \in ran (.) \to if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩) \in (\leq \cap (ℝ^{} \times ℝ^{}))$
50	1 49	fmpti	$⊢ F : ran (.) ⟶ \leq \cap (ℝ^{} \times ℝ^{})$

Metamath Proof Explorer

Theorem ioorf

Proof