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	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
	uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
Assertion	uniiccvol	$⊢ φ \to {vol}^{} (⋃ ran ([.] \circ F)) = sup (ran S ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
3		uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
4		ovolficcss	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ F) \subseteq ℝ$
5	1 4	syl	$⊢ φ \to ⋃ ran ([.] \circ F) \subseteq ℝ$
6		ovolcl	$⊢ ⋃ ran ([.] \circ F) \subseteq ℝ \to {vol}^{} (⋃ ran ([.] \circ F)) \in ℝ^{}$
7	5 6	syl	$⊢ φ \to {vol}^{} (⋃ ran ([.] \circ F)) \in ℝ^{}$
8		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
9	8 3	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
10	1 9	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
11	10	frnd	$⊢ φ \to ran S \subseteq [0, +∞)$
12		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
13	11 12	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
14		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
15	13 14	syl	$⊢ φ \to sup (ran S ℝ^{} <) \in ℝ^{}$
16		ssid	$⊢ ⋃ ran ([.] \circ F) \subseteq ⋃ ran ([.] \circ F)$
17	3	ovollb2	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ran ([.] \circ F) \subseteq ⋃ ran ([.] \circ F)) \to {vol}^{} (⋃ ran ([.] \circ F)) \leq sup (ran S ℝ^{} <)$
18	1 16 17	sylancl	$⊢ φ \to {vol}^{} (⋃ ran ([.] \circ F)) \leq sup (ran S ℝ^{} <)$
19	1 2 3	uniioovol	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ F)) = sup (ran S ℝ^{} <)$
20		ioossicc	$⊢ (1^{st} (F (x)), 2^{nd} (F (x))) \subseteq [1^{st} (F (x)), 2^{nd} (F (x))]$
21		df-ov	$⊢ (1^{st} (F (x)), 2^{nd} (F (x))) = (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
22		df-ov	$⊢ [1^{st} (F (x)), 2^{nd} (F (x))] = [.] (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
23	20 21 22	3sstr3i	$⊢ (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩) \subseteq [.] (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
24	23	a1i	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩) \subseteq [.] (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
25		ffvelrn	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to F (x) \in (\leq \cap ℝ^{2})$
26	25	elin2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to F (x) \in ℝ^{2}$
27		1st2nd2	$⊢ F (x) \in ℝ^{2} \to F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
28	26 27	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
29	28	fveq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to (.) (F (x)) = (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
30	28	fveq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to [.] (F (x)) = [.] (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
31	24 29 30	3sstr4d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to (.) (F (x)) \subseteq [.] (F (x))$
32		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to ((.) \circ F) (x) = (.) (F (x))$
33		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to ([.] \circ F) (x) = [.] (F (x))$
34	31 32 33	3sstr4d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to ((.) \circ F) (x) \subseteq ([.] \circ F) (x)$
35	1 34	sylan	$⊢ (φ \land x \in ℕ) \to ((.) \circ F) (x) \subseteq ([.] \circ F) (x)$
36	35	ralrimiva	$⊢ φ \to \forall x \in ℕ ((.) \circ F) (x) \subseteq ([.] \circ F) (x)$
37		ss2iun	$⊢ \forall x \in ℕ ((.) \circ F) (x) \subseteq ([.] \circ F) (x) \to ⋃_{x \in ℕ} ((.) \circ F) (x) \subseteq ⋃_{x \in ℕ} ([.] \circ F) (x)$
38	36 37	syl	$⊢ φ \to ⋃_{x \in ℕ} ((.) \circ F) (x) \subseteq ⋃_{x \in ℕ} ([.] \circ F) (x)$
39		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
40		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
41	39 40	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
42		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
43		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
44	42 43	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
45		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
46	1 44 45	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
47		fnfco	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) Fn ℕ$
48	41 46 47	sylancr	$⊢ φ \to ((.) \circ F) Fn ℕ$
49		fniunfv	$⊢ ((.) \circ F) Fn ℕ \to ⋃_{x \in ℕ} ((.) \circ F) (x) = ⋃ ran ((.) \circ F)$
50	48 49	syl	$⊢ φ \to ⋃_{x \in ℕ} ((.) \circ F) (x) = ⋃ ran ((.) \circ F)$
51		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
52		ffn	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \to [.] Fn (ℝ^{} \times ℝ^{*})$
53	51 52	ax-mp	$⊢ [.] Fn (ℝ^{} \times ℝ^{})$
54		fnfco	$⊢ ([.] Fn (ℝ^{} \times ℝ^{}) \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ([.] \circ F) Fn ℕ$
55	53 46 54	sylancr	$⊢ φ \to ([.] \circ F) Fn ℕ$
56		fniunfv	$⊢ ([.] \circ F) Fn ℕ \to ⋃_{x \in ℕ} ([.] \circ F) (x) = ⋃ ran ([.] \circ F)$
57	55 56	syl	$⊢ φ \to ⋃_{x \in ℕ} ([.] \circ F) (x) = ⋃ ran ([.] \circ F)$
58	38 50 57	3sstr3d	$⊢ φ \to ⋃ ran ((.) \circ F) \subseteq ⋃ ran ([.] \circ F)$
59		ovolss	$⊢ (⋃ ran ((.) \circ F) \subseteq ⋃ ran ([.] \circ F) \land ⋃ ran ([.] \circ F) \subseteq ℝ) \to {vol}^{} (⋃ ran ((.) \circ F)) \leq {vol}^{} (⋃ ran ([.] \circ F))$
60	58 5 59	syl2anc	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ F)) \leq {vol}^{} (⋃ ran ([.] \circ F))$
61	19 60	eqbrtrrd	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (⋃ ran ([.] \circ F))$
62	7 15 18 61	xrletrid	$⊢ φ \to {vol}^{} (⋃ ran ([.] \circ F)) = sup (ran S ℝ^{} <)$

Metamath Proof Explorer

Theorem uniiccvol

Proof