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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ovolval4lem2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
	ovolval4lem2.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
Assertion	ovolval4lem2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovolval4lem2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolval4lem2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
3		ovolval4lem2.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
4		iftrue	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
5	4	opeq2d	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
6	5	adantl	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
7		df-br	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ↔ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
8	7	biimpi	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
9	8	adantl	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
10	6 9	eqeltrd	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ≤ )
11		iffalse	⊢ ( ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
12	11	opeq2d	⊢ ( ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
13	12	adantl	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
14		elmapi	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
15	14	ffvelrnda	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
16		xp1st	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
17	15 16	syl	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
18	17	leidd	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
19		df-br	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ↔ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
20	18 19	sylib	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
21	20	adantr	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
22	13 21	eqeltrd	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ≤ )
23	10 22	pm2.61dan	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ≤ )
24		xp2nd	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
25	15 24	syl	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
26	25 17	ifcld	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ∈ ℝ )
27		opelxpi	⊢ ( ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ∈ ℝ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ( ℝ × ℝ ) )
28	17 26 27	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ( ℝ × ℝ ) )
29	23 28	elind	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
30	29 3	fmptd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
31		reex	⊢ ℝ ∈ V
32	31 31	xpex	⊢ ( ℝ × ℝ ) ∈ V
33	32	inex2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V
34	33	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V )
35		nnex	⊢ ℕ ∈ V
36	35	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ℕ ∈ V )
37	34 36	elmapd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )
38	30 37	mpbird	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
39	38	adantr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
40		simpr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) )
41		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
42	41	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* ) )
43	14 42	fssd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
44		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
45		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
46	44 45	breq12d	⊢ ( 𝑘 = 𝑛 → ( ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
47	46	cbvrabv	⊢ { 𝑘 ∈ ℕ ∣ ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) } = { 𝑛 ∈ ℕ ∣ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) }
48	43 3 47	ovolval4lem1	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐺 ) ∧ ( vol ∘ ( (,) ∘ 𝑓 ) ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) ) )
49	48	simpld	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐺 ) )
50	49	adantr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐺 ) )
51	40 50	sseqtrd	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
52	51	adantrr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
53		simpr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) )
54	48	simprd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( vol ∘ ( (,) ∘ 𝑓 ) ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) )
55		coass	⊢ ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( vol ∘ ( (,) ∘ 𝑓 ) )
56	55	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( vol ∘ ( (,) ∘ 𝑓 ) ) )
57		coass	⊢ ( ( vol ∘ (,) ) ∘ 𝐺 ) = ( vol ∘ ( (,) ∘ 𝐺 ) )
58	57	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝐺 ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) )
59	54 56 58	3eqtr4d	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( vol ∘ (,) ) ∘ 𝐺 ) )
60	59	fveq2d	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
61	60	adantr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
62	53 61	eqtrd	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
63	62	adantrl	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
64	52 63	jca	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) )
65		coeq2	⊢ ( 𝑔 = 𝐺 → ( (,) ∘ 𝑔 ) = ( (,) ∘ 𝐺 ) )
66	65	rneqd	⊢ ( 𝑔 = 𝐺 → ran ( (,) ∘ 𝑔 ) = ran ( (,) ∘ 𝐺 ) )
67	66	unieqd	⊢ ( 𝑔 = 𝐺 → ∪ ran ( (,) ∘ 𝑔 ) = ∪ ran ( (,) ∘ 𝐺 ) )
68	67	sseq2d	⊢ ( 𝑔 = 𝐺 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) )
69		coeq2	⊢ ( 𝑔 = 𝐺 → ( ( vol ∘ (,) ) ∘ 𝑔 ) = ( ( vol ∘ (,) ) ∘ 𝐺 ) )
70	69	fveq2d	⊢ ( 𝑔 = 𝐺 → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
71	70	eqeq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ↔ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) )
72	68 71	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) ) )
73	72	rspcev	⊢ ( ( 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
74	39 64 73	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
75	74	rexlimiva	⊢ ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
76		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
77		mapss	⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ ) )
78	32 76 77	mp2an	⊢ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ )
79	78	sseli	⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑔 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
80	79	adantr	⊢ ( ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → 𝑔 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
81		simpr	⊢ ( ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
82		coeq2	⊢ ( 𝑓 = 𝑔 → ( (,) ∘ 𝑓 ) = ( (,) ∘ 𝑔 ) )
83	82	rneqd	⊢ ( 𝑓 = 𝑔 → ran ( (,) ∘ 𝑓 ) = ran ( (,) ∘ 𝑔 ) )
84	83	unieqd	⊢ ( 𝑓 = 𝑔 → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝑔 ) )
85	84	sseq2d	⊢ ( 𝑓 = 𝑔 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) )
86		coeq2	⊢ ( 𝑓 = 𝑔 → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( vol ∘ (,) ) ∘ 𝑔 ) )
87	86	fveq2d	⊢ ( 𝑓 = 𝑔 → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) )
88	87	eqeq2d	⊢ ( 𝑓 = 𝑔 → ( 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
89	85 88	anbi12d	⊢ ( 𝑓 = 𝑔 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) )
90	89	rspcev	⊢ ( ( 𝑔 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
91	80 81 90	syl2anc	⊢ ( ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
92	91	rexlimiva	⊢ ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
93	75 92	impbii	⊢ ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
94	93	rabbii	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) }
95	2 94	eqtri	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) }
96	1 95	ovolval3	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem ovolval4lem2

Proof