uniiccvol

Description: An almost-disjoint union of closed intervals (disjoint interiors) has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) (Contributed by Mario Carneiro, 25-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2		uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3		uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4		ovolficcss	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
5	1 4	syl	⊢ ( 𝜑 → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
6		ovolcl	⊢ ( ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ → ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) ∈ ℝ^* )
7	5 6	syl	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) ∈ ℝ^* )
8		eqid	⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
9	8 3	ovolsf	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
10	1 9	syl	⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
11	10	frnd	⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
12		icossxr	⊢ ( 0 [,) +∞ ) ⊆ ℝ^*
13	11 12	sstrdi	⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ^* )
14		supxrcl	⊢ ( ran 𝑆 ⊆ ℝ^* → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ^* )
15	13 14	syl	⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ^* )
16		ssid	⊢ ∪ ran ( [,] ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 )
17	3	ovollb2	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ ran ( [,] ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
18	1 16 17	sylancl	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
19	1 2 3	uniioovol	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) = sup ( ran 𝑆 , ℝ^* , < ) )
20		ioossicc	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) [,] ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) )
21		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
22		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) [,] ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( [,] ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
23	20 21 22	3sstr3i	⊢ ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) ⊆ ( [,] ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
24	23	a1i	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) ⊆ ( [,] ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) )
25		ffvelcdm	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
26	25	elin2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) )
27		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
28	26 27	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
29	28	fveq2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) )
30	28	fveq2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑥 ) ) = ( [,] ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) )
31	24 29 30	3sstr4d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( [,] ‘ ( 𝐹 ‘ 𝑥 ) ) )
32		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
33		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) = ( [,] ‘ ( 𝐹 ‘ 𝑥 ) ) )
34	31 32 33	3sstr4d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) )
35	1 34	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) )
36	35	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) )
37		ss2iun	⊢ ( ∀ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) )
38	36 37	syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) )
39		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
40		ffn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ^* × ℝ^* ) )
41	39 40	ax-mp	⊢ (,) Fn ( ℝ^* × ℝ^* )
42		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
43		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
44	42 43	sstri	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* )
45		fss	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* ) ) → 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
46	1 44 45	sylancl	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
47		fnfco	⊢ ( ( (,) Fn ( ℝ^* × ℝ^* ) ∧ 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) ) → ( (,) ∘ 𝐹 ) Fn ℕ )
48	41 46 47	sylancr	⊢ ( 𝜑 → ( (,) ∘ 𝐹 ) Fn ℕ )
49		fniunfv	⊢ ( ( (,) ∘ 𝐹 ) Fn ℕ → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( (,) ∘ 𝐹 ) )
50	48 49	syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( (,) ∘ 𝐹 ) )
51		iccf	⊢ [,] : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*
52		ffn	⊢ ( [,] : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^* → [,] Fn ( ℝ^* × ℝ^* ) )
53	51 52	ax-mp	⊢ [,] Fn ( ℝ^* × ℝ^* )
54		fnfco	⊢ ( ( [,] Fn ( ℝ^* × ℝ^* ) ∧ 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) ) → ( [,] ∘ 𝐹 ) Fn ℕ )
55	53 46 54	sylancr	⊢ ( 𝜑 → ( [,] ∘ 𝐹 ) Fn ℕ )
56		fniunfv	⊢ ( ( [,] ∘ 𝐹 ) Fn ℕ → ∪ 𝑥 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( [,] ∘ 𝐹 ) )
57	55 56	syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑥 ) = ∪ ran ( [,] ∘ 𝐹 ) )
58	38 50 57	3sstr3d	⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) )
59		ovolss	⊢ ( ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) ∧ ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ≤ ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) )
60	58 5 59	syl2anc	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐹 ) ) ≤ ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) )
61	19 60	eqbrtrrd	⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) )
62	7 15 18 61	xrletrid	⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( [,] ∘ 𝐹 ) ) = sup ( ran 𝑆 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem uniiccvol

Proof