ioorcl

Description: The function F does not always return real numbers, but it does on intervals of finite volume. (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	ioorcl	$⊢ (A \in ran (.) \land {vol}^{*} (A) \in ℝ) \to F (A) \in (\leq \cap ℝ^{2})$

Proof

Step	Hyp	Ref	Expression
1		ioorf.1	$⊢ F = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨sup (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
2	1	ioorf	$⊢ F : ran (.) ⟶ \leq \cap (ℝ^{} \times ℝ^{})$
3	2	ffvelrni	$⊢ A \in ran (.) \to F (A) \in (\leq \cap (ℝ^{} \times ℝ^{}))$
4	3	adantr	$⊢ (A \in ran (.) \land {vol}^{} (A) \in ℝ) \to F (A) \in (\leq \cap (ℝ^{} \times ℝ^{*}))$
5	4	elin1d	$⊢ (A \in ran (.) \land {vol}^{*} (A) \in ℝ) \to F (A) \in \leq$
6	1	ioorval	$⊢ A \in ran (.) \to F (A) = if (A = \emptyset, ⟨0, 0⟩, ⟨sup (A ℝ^{} <), sup (A ℝ^{} <)⟩)$
7	6	adantr	$⊢ (A \in ran (.) \land {vol}^{} (A) \in ℝ) \to F (A) = if (A = \emptyset, ⟨0, 0⟩, ⟨sup (A ℝ^{} <), sup (A ℝ^{*} <)⟩)$
8		iftrue	$⊢ A = \emptyset \to if (A = \emptyset, ⟨0, 0⟩, ⟨sup (A ℝ^{} <), sup (A ℝ^{} <)⟩) = ⟨0, 0⟩$
9	7 8	sylan9eq	$⊢ ((A \in ran (.) \land {vol}^{*} (A) \in ℝ) \land A = \emptyset) \to F (A) = ⟨0, 0⟩$
10		0re	$⊢ 0 \in ℝ$
11		opelxpi	$⊢ (0 \in ℝ \land 0 \in ℝ) \to ⟨0, 0⟩ \in ℝ^{2}$
12	10 10 11	mp2an	$⊢ ⟨0, 0⟩ \in ℝ^{2}$
13	9 12	eqeltrdi	$⊢ ((A \in ran (.) \land {vol}^{*} (A) \in ℝ) \land A = \emptyset) \to F (A) \in ℝ^{2}$
14		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
15		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
16		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (A \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} A = (a, b))$
17	14 15 16	mp2b	$⊢ A \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} A = (a, b)$
18	1	ioorinv2	$⊢ (a, b) \neq \emptyset \to F ((a, b)) = ⟨a, b⟩$
19	18	adantl	$⊢ ({vol}^{*} ((a, b)) \in ℝ \land (a, b) \neq \emptyset) \to F ((a, b)) = ⟨a, b⟩$
20		ioorcl2	$⊢ ((a, b) \neq \emptyset \land {vol}^{*} ((a, b)) \in ℝ) \to (a \in ℝ \land b \in ℝ)$
21	20	ancoms	$⊢ ({vol}^{*} ((a, b)) \in ℝ \land (a, b) \neq \emptyset) \to (a \in ℝ \land b \in ℝ)$
22		opelxpi	$⊢ (a \in ℝ \land b \in ℝ) \to ⟨a, b⟩ \in ℝ^{2}$
23	21 22	syl	$⊢ ({vol}^{*} ((a, b)) \in ℝ \land (a, b) \neq \emptyset) \to ⟨a, b⟩ \in ℝ^{2}$
24	19 23	eqeltrd	$⊢ ({vol}^{*} ((a, b)) \in ℝ \land (a, b) \neq \emptyset) \to F ((a, b)) \in ℝ^{2}$
25		fveq2	$⊢ A = (a, b) \to {vol}^{} (A) = {vol}^{} ((a, b))$
26	25	eleq1d	$⊢ A = (a, b) \to ({vol}^{} (A) \in ℝ \leftrightarrow {vol}^{} ((a, b)) \in ℝ)$
27		neeq1	$⊢ A = (a, b) \to (A \neq \emptyset \leftrightarrow (a, b) \neq \emptyset)$
28	26 27	anbi12d	$⊢ A = (a, b) \to (({vol}^{} (A) \in ℝ \land A \neq \emptyset) \leftrightarrow ({vol}^{} ((a, b)) \in ℝ \land (a, b) \neq \emptyset))$
29		fveq2	$⊢ A = (a, b) \to F (A) = F ((a, b))$
30	29	eleq1d	$⊢ A = (a, b) \to (F (A) \in ℝ^{2} \leftrightarrow F ((a, b)) \in ℝ^{2})$
31	28 30	imbi12d	$⊢ A = (a, b) \to ((({vol}^{} (A) \in ℝ \land A \neq \emptyset) \to F (A) \in ℝ^{2}) \leftrightarrow (({vol}^{} ((a, b)) \in ℝ \land (a, b) \neq \emptyset) \to F ((a, b)) \in ℝ^{2}))$
32	24 31	mpbiri	$⊢ A = (a, b) \to (({vol}^{*} (A) \in ℝ \land A \neq \emptyset) \to F (A) \in ℝ^{2})$
33	32	a1i	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (A = (a, b) \to (({vol}^{*} (A) \in ℝ \land A \neq \emptyset) \to F (A) \in ℝ^{2}))$
34	33	rexlimivv	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} A = (a, b) \to (({vol}^{*} (A) \in ℝ \land A \neq \emptyset) \to F (A) \in ℝ^{2})$
35	17 34	sylbi	$⊢ A \in ran (.) \to (({vol}^{*} (A) \in ℝ \land A \neq \emptyset) \to F (A) \in ℝ^{2})$
36	35	impl	$⊢ ((A \in ran (.) \land {vol}^{*} (A) \in ℝ) \land A \neq \emptyset) \to F (A) \in ℝ^{2}$
37	13 36	pm2.61dane	$⊢ (A \in ran (.) \land {vol}^{*} (A) \in ℝ) \to F (A) \in ℝ^{2}$
38	5 37	elind	$⊢ (A \in ran (.) \land {vol}^{*} (A) \in ℝ) \to F (A) \in (\leq \cap ℝ^{2})$

Metamath Proof Explorer

Theorem ioorcl

Proof