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

Metamath Proof Explorer

Theorem ovolval4lem2

Proof