Theorem uniioovol 25614

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 25589.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.)

Hypotheses

Ref	Expression
uniioombl.1	⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2	⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
uniioombl.3	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))

Assertion

Ref	Expression
uniioovol	⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))

Distinct variable groups:   𝑥,𝐹   𝜑,𝑥

Allowed substitution hint:   𝑆(𝑥)

Proof of Theorem uniioovol

Dummy variables 𝑛 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ioof 13487	. . . . . 6 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2		uniioombl.1	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3		inss2 4238	. . . . . . . 8 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
4		rexpssxrxp 11306	. . . . . . . 8 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
5	3, 4	sstri 3993	. . . . . . 7 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
6		fss 6752	. . . . . . 7 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
7	2, 5, 6	sylancl 586	. . . . . 6 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
8		fco 6760	. . . . . 6 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
9	1, 7, 8	sylancr 587	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
10	9	frnd 6744	. . . 4 ⊢ (𝜑 → ran ((,) ∘ 𝐹) ⊆ 𝒫 ℝ)
11		sspwuni 5100	. . . 4 ⊢ (ran ((,) ∘ 𝐹) ⊆ 𝒫 ℝ ↔ ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
12	10, 11	sylib 218	. . 3 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
13		ovolcl 25513	. . 3 ⊢ (∪ ran ((,) ∘ 𝐹) ⊆ ℝ → (vol*‘∪ ran ((,) ∘ 𝐹)) ∈ ℝ*)
14	12, 13	syl 17	. 2 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ∈ ℝ*)
15		eqid 2737	. . . . . 6 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
16		uniioombl.3	. . . . . 6 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
17	15, 16	ovolsf 25507	. . . . 5 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
18		frn 6743	. . . . 5 ⊢ (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
19	2, 17, 18	3syl 18	. . . 4 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
20		icossxr 13472	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ*
21	19, 20	sstrdi 3996	. . 3 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ*)
22		supxrcl 13357	. . 3 ⊢ (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
23	21, 22	syl 17	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
24		ssid 4006	. . 3 ⊢ ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ((,) ∘ 𝐹)
25	16	ovollb 25514	. . 3 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ((,) ∘ 𝐹)) → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, < ))
26	2, 24, 25	sylancl 586	. 2 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, < ))
27	16	fveq1i 6907	. . . . . . . 8 ⊢ (𝑆‘𝑛) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑛)
28	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
29		elfznn 13593	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝑛) → 𝑥 ∈ ℕ)
30	15	ovolfsval 25505	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑥) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))))
31	28, 29, 30	syl2an 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ 𝐹)‘𝑥) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))))
32		fvco3 7008	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥)))
33	28, 29, 32	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥)))
34		ffvelcdm 7101	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ × ℝ)))
35	28, 29, 34	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ × ℝ)))
36	35	elin2d 4205	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) ∈ (ℝ × ℝ))
37		1st2nd2 8053	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) ∈ (ℝ × ℝ) → (𝐹‘𝑥) = ⟨(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))⟩)
38	36, 37	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) = ⟨(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))⟩)
39	38	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹‘𝑥)) = ((,)‘⟨(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))⟩))
40		df-ov 7434	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) = ((,)‘⟨(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))⟩)
41	39, 40	eqtr4di 2795	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹‘𝑥)) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))))
42	33, 41	eqtrd 2777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))))
43		ioombl 25600	. . . . . . . . . . . . 13 ⊢ ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∈ dom vol
44	42, 43	eqeltrdi 2849	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
45		mblvol 25565	. . . . . . . . . . . 12 ⊢ ((((,) ∘ 𝐹)‘𝑥) ∈ dom vol → (vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥)))
46	44, 45	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥)))
47	42	fveq2d 6910	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))))
48		ovolfcl 25501	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))))
49	28, 29, 48	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))))
50		ovolioo 25603	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) → (vol*‘((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))))
51	49, 50	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))))
52	46, 47, 51	3eqtrd 2781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))))
53	31, 52	eqtr4d 2780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ 𝐹)‘𝑥) = (vol‘(((,) ∘ 𝐹)‘𝑥)))
54		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
55		nnuz 12921	. . . . . . . . . 10 ⊢ ℕ = (ℤ≥‘1)
56	54, 55	eleqtrdi 2851	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ≥‘1))
57	49	simp2d 1144	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (2nd ‘(𝐹‘𝑥)) ∈ ℝ)
58	49	simp1d 1143	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (1st ‘(𝐹‘𝑥)) ∈ ℝ)
59	57, 58	resubcld 11691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))) ∈ ℝ)
60	52, 59	eqeltrd 2841	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ)
61	60	recnd 11289	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℂ)
62	53, 56, 61	fsumser 15766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑛))
63	27, 62	eqtr4id 2796	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)))
64		fzfid 14014	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
65	44, 60	jca 511	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ))
66	65	ralrimiva 3146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ))
67		fz1ssnn 13595	. . . . . . . . 9 ⊢ (1...𝑛) ⊆ ℕ
68		uniioombl.2	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
69	2, 32	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥)))
70	69	disjeq2dv 5115	. . . . . . . . . . 11 ⊢ (𝜑 → (Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ↔ Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))))
71	68, 70	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
72	71	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
73		disjss1 5116	. . . . . . . . 9 ⊢ ((1...𝑛) ⊆ ℕ → (Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
74	67, 72, 73	mpsyl 68	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))
75		volfiniun 25582	. . . . . . . 8 ⊢ (((1...𝑛) ∈ Fin ∧ ∀𝑥 ∈ (1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ) ∧ Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)))
76	64, 66, 74, 75	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)))
77	44	ralrimiva 3146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
78		finiunmbl 25579	. . . . . . . . 9 ⊢ (((1...𝑛) ∈ Fin ∧ ∀𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
79	64, 77, 78	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol)
80		mblvol 25565	. . . . . . . 8 ⊢ (∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
81	79, 80	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
82	63, 76, 81	3eqtr2d 2783	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)))
83		iunss1 5006	. . . . . . . . 9 ⊢ ((1...𝑛) ⊆ ℕ → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
84	67, 83	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥))
85	9	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
86		ffn 6736	. . . . . . . . 9 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
87		fniunfv 7267	. . . . . . . . 9 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,) ∘ 𝐹))
88	85, 86, 87	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,) ∘ 𝐹))
89	84, 88	sseqtrd 4020	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ ran ((,) ∘ 𝐹))
90	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
91		ovolss 25520	. . . . . . 7 ⊢ ((∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ ran ((,) ∘ 𝐹) ∧ ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) → (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))
92	89, 90, 91	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))
93	82, 92	eqbrtrd 5165	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))
94	93	ralrimiva 3146	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))
95	2, 17	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
96		ffn 6736	. . . . 5 ⊢ (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
97		breq1 5146	. . . . . 6 ⊢ (𝑦 = (𝑆‘𝑛) → (𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))))
98	97	ralrn 7108	. . . . 5 ⊢ (𝑆 Fn ℕ → (∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))))
99	95, 96, 98	3syl 18	. . . 4 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))))
100	94, 99	mpbird 257	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))
101		supxrleub 13368	. . . 4 ⊢ ((ran 𝑆 ⊆ ℝ* ∧ (vol*‘∪ ran ((,) ∘ 𝐹)) ∈ ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹))))
102	21, 14, 101	syl2anc 584	. . 3 ⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹))))
103	100, 102	mpbird 257	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))
104	14, 23, 26, 103	xrletrid 13197	1 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061   ∩ cin 3950   ⊆ wss 3951  𝒫 cpw 4600  ⟨cop 4632  ∪ cuni 4907  ∪ ciun 4991  Disj wdisj 5110   class class class wbr 5143   × cxp 5683  dom cdm 5685  ran crn 5686   ∘ ccom 5689   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561  (class class class)co 7431  1^st c1st 8012  2^nd c2nd 8013  Fincfn 8985  supcsup 9480  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158  +∞cpnf 11292  ℝ^*cxr 11294   < clt 11295   ≤ cle 11296   − cmin 11492  ℕcn 12266  ℤ_≥cuz 12878  (,)cioo 13387  [,)cico 13389  ...cfz 13547  seqcseq 14042  abscabs 15273  Σcsu 15722  vol*covol 25497  volcvol 25498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-rest 17467  df-topgen 17488  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-top 22900  df-topon 22917  df-bases 22953  df-cmp 23395  df-ovol 25499  df-vol 25500

This theorem is referenced by:  uniiccvol  25615  uniioombllem2  25618