ovolval4lem2

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval4lem2.a	$⊢ φ \to A \subseteq ℝ$
	ovolval4lem2.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\}$
	ovolval4lem2.g	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩)$
Assertion	ovolval4lem2	$⊢ φ \to {vol}^{} (A) = inf (M ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		ovolval4lem2.a	$⊢ φ \to A \subseteq ℝ$
2		ovolval4lem2.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\}$
3		ovolval4lem2.g	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩)$
4		iftrue	$⊢ 1^{st} (f (n)) \leq 2^{nd} (f (n)) \to if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n))) = 2^{nd} (f (n))$
5	4	opeq2d	$⊢ 1^{st} (f (n)) \leq 2^{nd} (f (n)) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ = ⟨1^{st} (f (n)), 2^{nd} (f (n))⟩$
6	5	adantl	$⊢ ((f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \land 1^{st} (f (n)) \leq 2^{nd} (f (n))) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ = ⟨1^{st} (f (n)), 2^{nd} (f (n))⟩$
7		df-br	$⊢ 1^{st} (f (n)) \leq 2^{nd} (f (n)) \leftrightarrow ⟨1^{st} (f (n)), 2^{nd} (f (n))⟩ \in \leq$
8	7	bilani	$⊢ ((f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \land 1^{st} (f (n)) \leq 2^{nd} (f (n))) \to ⟨1^{st} (f (n)), 2^{nd} (f (n))⟩ \in \leq$
9	6 8	eqeltrd	$⊢ ((f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \land 1^{st} (f (n)) \leq 2^{nd} (f (n))) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ \in \leq$
10		iffalse	$⊢ \neg 1^{st} (f (n)) \leq 2^{nd} (f (n)) \to if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n))) = 1^{st} (f (n))$
11	10	opeq2d	$⊢ \neg 1^{st} (f (n)) \leq 2^{nd} (f (n)) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ = ⟨1^{st} (f (n)), 1^{st} (f (n))⟩$
12	11	adantl	$⊢ ((f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \land \neg 1^{st} (f (n)) \leq 2^{nd} (f (n))) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ = ⟨1^{st} (f (n)), 1^{st} (f (n))⟩$
13		elmapi	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to f : ℕ ⟶ ℝ^{2}$
14	13	ffvelcdmda	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to f (n) \in ℝ^{2}$
15		xp1st	$⊢ f (n) \in ℝ^{2} \to 1^{st} (f (n)) \in ℝ$
16	14 15	syl	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to 1^{st} (f (n)) \in ℝ$
17	16	leidd	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to 1^{st} (f (n)) \leq 1^{st} (f (n))$
18		df-br	$⊢ 1^{st} (f (n)) \leq 1^{st} (f (n)) \leftrightarrow ⟨1^{st} (f (n)), 1^{st} (f (n))⟩ \in \leq$
19	17 18	sylib	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ⟨1^{st} (f (n)), 1^{st} (f (n))⟩ \in \leq$
20	19	adantr	$⊢ ((f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \land \neg 1^{st} (f (n)) \leq 2^{nd} (f (n))) \to ⟨1^{st} (f (n)), 1^{st} (f (n))⟩ \in \leq$
21	12 20	eqeltrd	$⊢ ((f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \land \neg 1^{st} (f (n)) \leq 2^{nd} (f (n))) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ \in \leq$
22	9 21	pm2.61dan	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ \in \leq$
23		xp2nd	$⊢ f (n) \in ℝ^{2} \to 2^{nd} (f (n)) \in ℝ$
24	14 23	syl	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to 2^{nd} (f (n)) \in ℝ$
25	24 16	ifcld	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n))) \in ℝ$
26		opelxpi	$⊢ (1^{st} (f (n)) \in ℝ \land if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n))) \in ℝ) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ \in ℝ^{2}$
27	16 25 26	syl2anc	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ \in ℝ^{2}$
28	22 27	elind	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ⟨1^{st} (f (n)), if (1^{st} (f (n)) \leq 2^{nd} (f (n)), 2^{nd} (f (n)), 1^{st} (f (n)))⟩ \in (\leq \cap ℝ^{2})$
29	28 3	fmptd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
30		reex	$⊢ ℝ \in V$
31	30 30	xpex	$⊢ ℝ^{2} \in V$
32	31	inex2	$⊢ \leq \cap ℝ^{2} \in V$
33	32	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to \leq \cap ℝ^{2} \in V$
34		nnex	$⊢ ℕ \in V$
35	34	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ℕ \in V$
36	33 35	elmapd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (G \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow G : ℕ ⟶ \leq \cap ℝ^{2})$
37	29 36	mpbird	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to G \in ({(\leq \cap ℝ^{2})}^{ℕ})$
38	37	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to G \in ({(\leq \cap ℝ^{2})}^{ℕ})$
39		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to A \subseteq ⋃ ran ((.) \circ f)$
40		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
41	40	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
42	13 41	fssd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to f : ℕ ⟶ ℝ^{} \times ℝ^{}$
43		2fveq3	$⊢ k = n \to 1^{st} (f (k)) = 1^{st} (f (n))$
44		2fveq3	$⊢ k = n \to 2^{nd} (f (k)) = 2^{nd} (f (n))$
45	43 44	breq12d	$⊢ k = n \to (1^{st} (f (k)) \leq 2^{nd} (f (k)) \leftrightarrow 1^{st} (f (n)) \leq 2^{nd} (f (n)))$
46	45	cbvrabv	$⊢ \{k \in ℕ \| 1^{st} (f (k)) \leq 2^{nd} (f (k))\} = \{n \in ℕ \| 1^{st} (f (n)) \leq 2^{nd} (f (n))\}$
47	42 3 46	ovolval4lem1	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (⋃ ran ((.) \circ f) = ⋃ ran ((.) \circ G) \land vol \circ ((.) \circ f) = vol \circ ((.) \circ G))$
48	47	simpld	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃ ran ((.) \circ f) = ⋃ ran ((.) \circ G)$
49	48	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to ⋃ ran ((.) \circ f) = ⋃ ran ((.) \circ G)$
50	39 49	sseqtrd	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to A \subseteq ⋃ ran ((.) \circ G)$
51	50	adantrr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to A \subseteq ⋃ ran ((.) \circ G)$
52		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to y = sum^((vol \circ (.)) \circ f)$
53	47	simprd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to vol \circ ((.) \circ f) = vol \circ ((.) \circ G)$
54		coass	$⊢ (vol \circ (.)) \circ f = vol \circ ((.) \circ f)$
55	54	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (vol \circ (.)) \circ f = vol \circ ((.) \circ f)$
56		coass	$⊢ (vol \circ (.)) \circ G = vol \circ ((.) \circ G)$
57	56	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (vol \circ (.)) \circ G = vol \circ ((.) \circ G)$
58	53 55 57	3eqtr4d	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (vol \circ (.)) \circ f = (vol \circ (.)) \circ G$
59	58	fveq2d	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ (.)) \circ G)$
60	59	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ (.)) \circ G)$
61	52 60	eqtrd	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to y = sum^((vol \circ (.)) \circ G)$
62	61	adantrl	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to y = sum^((vol \circ (.)) \circ G)$
63	51 62	jca	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to (A \subseteq ⋃ ran ((.) \circ G) \land y = sum^((vol \circ (.)) \circ G))$
64		coeq2	$⊢ g = G \to (.) \circ g = (.) \circ G$
65	64	rneqd	$⊢ g = G \to ran ((.) \circ g) = ran ((.) \circ G)$
66	65	unieqd	$⊢ g = G \to ⋃ ran ((.) \circ g) = ⋃ ran ((.) \circ G)$
67	66	sseq2d	$⊢ g = G \to (A \subseteq ⋃ ran ((.) \circ g) \leftrightarrow A \subseteq ⋃ ran ((.) \circ G))$
68		coeq2	$⊢ g = G \to (vol \circ (.)) \circ g = (vol \circ (.)) \circ G$
69	68	fveq2d	$⊢ g = G \to sum^((vol \circ (.)) \circ g) = sum^((vol \circ (.)) \circ G)$
70	69	eqeq2d	$⊢ g = G \to (y = sum^((vol \circ (.)) \circ g) \leftrightarrow y = sum^((vol \circ (.)) \circ G))$
71	67 70	anbi12d	$⊢ g = G \to ((A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ G) \land y = sum^((vol \circ (.)) \circ G)))$
72	71	rspcev	$⊢ (G \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ G) \land y = sum^((vol \circ (.)) \circ G))) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))$
73	38 63 72	syl2anc	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))$
74	73	rexlimiva	$⊢ \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))$
75		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
76		mapss	$⊢ (ℝ^{2} \in V \land \leq \cap ℝ^{2} \subseteq ℝ^{2}) \to {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
77	31 75 76	mp2an	$⊢ {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
78	77	sseli	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to g \in ({ℝ^{2}}^{ℕ})$
79	78	adantr	$⊢ (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))) \to g \in ({ℝ^{2}}^{ℕ})$
80		simpr	$⊢ (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))) \to (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))$
81		coeq2	$⊢ f = g \to (.) \circ f = (.) \circ g$
82	81	rneqd	$⊢ f = g \to ran ((.) \circ f) = ran ((.) \circ g)$
83	82	unieqd	$⊢ f = g \to ⋃ ran ((.) \circ f) = ⋃ ran ((.) \circ g)$
84	83	sseq2d	$⊢ f = g \to (A \subseteq ⋃ ran ((.) \circ f) \leftrightarrow A \subseteq ⋃ ran ((.) \circ g))$
85		coeq2	$⊢ f = g \to (vol \circ (.)) \circ f = (vol \circ (.)) \circ g$
86	85	fveq2d	$⊢ f = g \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ (.)) \circ g)$
87	86	eqeq2d	$⊢ f = g \to (y = sum^((vol \circ (.)) \circ f) \leftrightarrow y = sum^((vol \circ (.)) \circ g))$
88	84 87	anbi12d	$⊢ f = g \to ((A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)))$
89	88	rspcev	$⊢ (g \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))$
90	79 80 89	syl2anc	$⊢ (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))$
91	90	rexlimiva	$⊢ \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))$
92	74 91	impbii	$⊢ \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \leftrightarrow \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))$
93	92	rabbii	$⊢ \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\} = \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))\}$
94	2 93	eqtri	$⊢ M = \{y \in ℝ^{*} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g))\}$
95	1 94	ovolval3	$⊢ φ \to {vol}^{} (A) = inf (M ℝ^{} <)$

Metamath Proof Explorer

Theorem ovolval4lem2

Proof