uniioovol

Description: A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) Lemma 565Ca of Fremlin5 p. 213. (Contributed by Mario Carneiro, 26-Mar-2015)

	Ref	Expression
Hypotheses	uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
	uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
Assertion	uniioovol	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) = sup ( ran 𝑆 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2		uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3		uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
5		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
6		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
7	5 6	sstri	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* )
8		fss	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* ) ) → 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
9	1 7 8	sylancl	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
10		fco	⊢ ( ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ ∧ 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
11	4 9 10	sylancr	⊢ ( 𝜑 → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
12	11	frnd	⊢ ( 𝜑 → ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ )
13		sspwuni	⊢ ( ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ ↔ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
14	12 13	sylib	⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
15		ovolcl	⊢ ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ ℝ^* )
16	14 15	syl	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ ℝ^* )
17		eqid	⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
18	17 3	ovolsf	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
19		frn	⊢ ( 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
20	1 18 19	3syl	⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
21		icossxr	⊢ ( 0 [,) +∞ ) ⊆ ℝ^*
22	20 21	sstrdi	⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ^* )
23		supxrcl	⊢ ( ran 𝑆 ⊆ ℝ^* → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ^* )
24	22 23	syl	⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ^* )
25		ssid	⊢ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( (,) ∘ 𝐹 )
26	3	ovollb	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
27	1 25 26	sylancl	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
28	3	fveq1i	⊢ ( 𝑆 ‘ 𝑛 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑛 )
29	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
30		elfznn	⊢ ( 𝑥 ∈ ( 1 ... 𝑛 ) → 𝑥 ∈ ℕ )
31	17	ovolfsval	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
32	29 30 31	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
33		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
34	29 30 33	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
35		ffvelcdm	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
36	29 30 35	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
37	36	elin2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) )
38		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
39	37 38	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
40	39	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) )
41		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
42	40 41	eqtr4di	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
43	34 42	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
44		ioombl	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ dom vol
45	43 44	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
46		mblvol	⊢ ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
47	45 46	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
48	43	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
49		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
50	29 30 49	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
51		ovolioo	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( vol* ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
52	50 51	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
53	47 48 52	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
54	32 53	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑥 ) = ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
55		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
56		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
57	55 56	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ_≥ ‘ 1 ) )
58	50	simp2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
59	50	simp1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
60	58 59	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
61	53 60	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ )
62	61	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℂ )
63	54 57 62	fsumser	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑛 ) )
64	28 63	eqtr4id	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ‘ 𝑛 ) = Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
65		fzfid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
66	45 61	jca	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑛 ) ) → ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ ) )
67	66	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ ) )
68		fz1ssnn	⊢ ( 1 ... 𝑛 ) ⊆ ℕ
69	1 33	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
70	69	disjeq2dv	⊢ ( 𝜑 → ( Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ↔ Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
71	2 70	mpbird	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
73		disjss1	⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ( Disj 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) → Disj 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
74	68 72 73	mpsyl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
75		volfiniun	⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ ) ∧ Disj 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
76	65 67 74 75	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = Σ 𝑥 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
77	45	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
78		finiunmbl	⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
79	65 77 78	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
80		mblvol	⊢ ( ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
81	79 80	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
82	64 76 81	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ‘ 𝑛 ) = ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) )
83		iunss1	⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
84	68 83	mp1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) )
85	11	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
86		ffn	⊢ ( ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ → ( (,) ∘ 𝐹 ) Fn ℕ )
87		fniunfv	⊢ ( ( (,) ∘ 𝐹 ) Fn ℕ → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( (,) ∘ 𝐹 ) )
88	85 86 87	3syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( (,) ∘ 𝐹 ) )
89	84 88	sseqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
90	14	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
91		ovolss	⊢ ( ( ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ ran ( (,) ∘ 𝐹 ) ∧ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ ) → ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
92	89 90 91	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ∪ 𝑥 ∈ ( 1 ... 𝑛 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
93	82 92	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
94	93	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
95	1 18	syl	⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
96		ffn	⊢ ( 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) → 𝑆 Fn ℕ )
97		breq1	⊢ ( 𝑦 = ( 𝑆 ‘ 𝑛 ) → ( 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
98	97	ralrn	⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
99	95 96 98	3syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
100	94 99	mpbird	⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
101		supxrleub	⊢ ( ( ran 𝑆 ⊆ ℝ^* ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ ℝ^* ) → ( sup ( ran 𝑆 , ℝ^* , < ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
102	22 16 101	syl2anc	⊢ ( 𝜑 → ( sup ( ran 𝑆 , ℝ^* , < ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ↔ ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ) )
103	100 102	mpbird	⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) )
104	16 24 27 103	xrletrid	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) = sup ( ran 𝑆 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem uniioovol

Proof