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	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
	uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
Assertion	uniioovol	$⊢ φ \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		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
5		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
6		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
7	5 6	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
8		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
9	1 7 8	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
10		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
11	4 9 10	sylancr	$⊢ φ \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
12	11	frnd	$⊢ φ \to ran ((.) \circ F) \subseteq 𝒫 ℝ$
13		sspwuni	$⊢ ran ((.) \circ F) \subseteq 𝒫 ℝ \leftrightarrow ⋃ ran ((.) \circ F) \subseteq ℝ$
14	12 13	sylib	$⊢ φ \to ⋃ ran ((.) \circ F) \subseteq ℝ$
15		ovolcl	$⊢ ⋃ ran ((.) \circ F) \subseteq ℝ \to {vol}^{} (⋃ ran ((.) \circ F)) \in ℝ^{}$
16	14 15	syl	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ F)) \in ℝ^{}$
17		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
18	17 3	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
19		frn	$⊢ S : ℕ ⟶ [0, +∞) \to ran S \subseteq [0, +∞)$
20	1 18 19	3syl	$⊢ φ \to ran S \subseteq [0, +∞)$
21		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
22	20 21	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
23		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
24	22 23	syl	$⊢ φ \to sup (ran S ℝ^{} <) \in ℝ^{}$
25		ssid	$⊢ ⋃ ran ((.) \circ F) \subseteq ⋃ ran ((.) \circ F)$
26	3	ovollb	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ran ((.) \circ F) \subseteq ⋃ ran ((.) \circ F)) \to {vol}^{} (⋃ ran ((.) \circ F)) \leq sup (ran S ℝ^{} <)$
27	1 25 26	sylancl	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ F)) \leq sup (ran S ℝ^{} <)$
28	3	fveq1i	$⊢ S (n) = seq 1 (+ ((abs \circ -) \circ F)) (n)$
29	1	adantr	$⊢ (φ \land n \in ℕ) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
30		elfznn	$⊢ x \in (1 \dots n) \to x \in ℕ$
31	17	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to ((abs \circ -) \circ F) (x) = 2^{nd} (F (x)) - 1^{st} (F (x))$
32	29 30 31	syl2an	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to ((abs \circ -) \circ F) (x) = 2^{nd} (F (x)) - 1^{st} (F (x))$
33		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to ((.) \circ F) (x) = (.) (F (x))$
34	29 30 33	syl2an	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to ((.) \circ F) (x) = (.) (F (x))$
35		ffvelrn	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to F (x) \in (\leq \cap ℝ^{2})$
36	29 30 35	syl2an	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to F (x) \in (\leq \cap ℝ^{2})$
37	36	elin2d	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to F (x) \in ℝ^{2}$
38		1st2nd2	$⊢ F (x) \in ℝ^{2} \to F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
39	37 38	syl	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
40	39	fveq2d	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to (.) (F (x)) = (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
41		df-ov	$⊢ (1^{st} (F (x)), 2^{nd} (F (x))) = (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
42	40 41	eqtr4di	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to (.) (F (x)) = (1^{st} (F (x)), 2^{nd} (F (x)))$
43	34 42	eqtrd	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to ((.) \circ F) (x) = (1^{st} (F (x)), 2^{nd} (F (x)))$
44		ioombl	$⊢ (1^{st} (F (x)), 2^{nd} (F (x))) \in dom vol$
45	43 44	eqeltrdi	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to ((.) \circ F) (x) \in dom vol$
46		mblvol	$⊢ ((.) \circ F) (x) \in dom vol \to vol (((.) \circ F) (x)) = {vol}^{*} (((.) \circ F) (x))$
47	45 46	syl	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to vol (((.) \circ F) (x)) = {vol}^{*} (((.) \circ F) (x))$
48	43	fveq2d	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to {vol}^{} (((.) \circ F) (x)) = {vol}^{} ((1^{st} (F (x)), 2^{nd} (F (x))))$
49		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ \land 1^{st} (F (x)) \leq 2^{nd} (F (x)))$
50	29 30 49	syl2an	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ \land 1^{st} (F (x)) \leq 2^{nd} (F (x)))$
51		ovolioo	$⊢ (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ \land 1^{st} (F (x)) \leq 2^{nd} (F (x))) \to {vol}^{*} ((1^{st} (F (x)), 2^{nd} (F (x)))) = 2^{nd} (F (x)) - 1^{st} (F (x))$
52	50 51	syl	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to {vol}^{*} ((1^{st} (F (x)), 2^{nd} (F (x)))) = 2^{nd} (F (x)) - 1^{st} (F (x))$
53	47 48 52	3eqtrd	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to vol (((.) \circ F) (x)) = 2^{nd} (F (x)) - 1^{st} (F (x))$
54	32 53	eqtr4d	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to ((abs \circ -) \circ F) (x) = vol (((.) \circ F) (x))$
55		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
56		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
57	55 56	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n \in ℤ_{\geq 1}$
58	50	simp2d	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to 2^{nd} (F (x)) \in ℝ$
59	50	simp1d	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to 1^{st} (F (x)) \in ℝ$
60	58 59	resubcld	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to 2^{nd} (F (x)) - 1^{st} (F (x)) \in ℝ$
61	53 60	eqeltrd	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to vol (((.) \circ F) (x)) \in ℝ$
62	61	recnd	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to vol (((.) \circ F) (x)) \in ℂ$
63	54 57 62	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{x = 1}^{n} vol (((.) \circ F) (x)) = seq 1 (+ ((abs \circ -) \circ F)) (n)$
64	28 63	eqtr4id	$⊢ (φ \land n \in ℕ) \to S (n) = \sum_{x = 1}^{n} vol (((.) \circ F) (x))$
65		fzfid	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \in Fin$
66	45 61	jca	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n)) \to (((.) \circ F) (x) \in dom vol \land vol (((.) \circ F) (x)) \in ℝ)$
67	66	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall x \in (1 \dots n) (((.) \circ F) (x) \in dom vol \land vol (((.) \circ F) (x)) \in ℝ)$
68		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
69	1 33	sylan	$⊢ (φ \land x \in ℕ) \to ((.) \circ F) (x) = (.) (F (x))$
70	69	disjeq2dv	$⊢ φ \to (\underset{x \in ℕ}{Disj} ((.) \circ F) (x) \leftrightarrow \underset{x \in ℕ}{Disj} (.) (F (x)))$
71	2 70	mpbird	$⊢ φ \to \underset{x \in ℕ}{Disj} ((.) \circ F) (x)$
72	71	adantr	$⊢ (φ \land n \in ℕ) \to \underset{x \in ℕ}{Disj} ((.) \circ F) (x)$
73		disjss1	$⊢ (1 \dots n) \subseteq ℕ \to (\underset{x \in ℕ}{Disj} ((.) \circ F) (x) \to {Disj}_{x = 1}^{n} ((.) \circ F) (x))$
74	68 72 73	mpsyl	$⊢ (φ \land n \in ℕ) \to {Disj}_{x = 1}^{n} ((.) \circ F) (x)$
75		volfiniun	$⊢ ((1 \dots n) \in Fin \land \forall x \in (1 \dots n) (((.) \circ F) (x) \in dom vol \land vol (((.) \circ F) (x)) \in ℝ) \land {Disj}_{x = 1}^{n} ((.) \circ F) (x)) \to vol (⋃_{x = 1}^{n} ((.) \circ F) (x)) = \sum_{x = 1}^{n} vol (((.) \circ F) (x))$
76	65 67 74 75	syl3anc	$⊢ (φ \land n \in ℕ) \to vol (⋃_{x = 1}^{n} ((.) \circ F) (x)) = \sum_{x = 1}^{n} vol (((.) \circ F) (x))$
77	45	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall x \in (1 \dots n) ((.) \circ F) (x) \in dom vol$
78		finiunmbl	$⊢ ((1 \dots n) \in Fin \land \forall x \in (1 \dots n) ((.) \circ F) (x) \in dom vol) \to ⋃_{x = 1}^{n} ((.) \circ F) (x) \in dom vol$
79	65 77 78	syl2anc	$⊢ (φ \land n \in ℕ) \to ⋃_{x = 1}^{n} ((.) \circ F) (x) \in dom vol$
80		mblvol	$⊢ ⋃_{x = 1}^{n} ((.) \circ F) (x) \in dom vol \to vol (⋃_{x = 1}^{n} ((.) \circ F) (x)) = {vol}^{*} (⋃_{x = 1}^{n} ((.) \circ F) (x))$
81	79 80	syl	$⊢ (φ \land n \in ℕ) \to vol (⋃_{x = 1}^{n} ((.) \circ F) (x)) = {vol}^{*} (⋃_{x = 1}^{n} ((.) \circ F) (x))$
82	64 76 81	3eqtr2d	$⊢ (φ \land n \in ℕ) \to S (n) = {vol}^{*} (⋃_{x = 1}^{n} ((.) \circ F) (x))$
83		iunss1	$⊢ (1 \dots n) \subseteq ℕ \to ⋃_{x = 1}^{n} ((.) \circ F) (x) \subseteq ⋃_{x \in ℕ} ((.) \circ F) (x)$
84	68 83	mp1i	$⊢ (φ \land n \in ℕ) \to ⋃_{x = 1}^{n} ((.) \circ F) (x) \subseteq ⋃_{x \in ℕ} ((.) \circ F) (x)$
85	11	adantr	$⊢ (φ \land n \in ℕ) \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
86		ffn	$⊢ ((.) \circ F) : ℕ ⟶ 𝒫 ℝ \to ((.) \circ F) Fn ℕ$
87		fniunfv	$⊢ ((.) \circ F) Fn ℕ \to ⋃_{x \in ℕ} ((.) \circ F) (x) = ⋃ ran ((.) \circ F)$
88	85 86 87	3syl	$⊢ (φ \land n \in ℕ) \to ⋃_{x \in ℕ} ((.) \circ F) (x) = ⋃ ran ((.) \circ F)$
89	84 88	sseqtrd	$⊢ (φ \land n \in ℕ) \to ⋃_{x = 1}^{n} ((.) \circ F) (x) \subseteq ⋃ ran ((.) \circ F)$
90	14	adantr	$⊢ (φ \land n \in ℕ) \to ⋃ ran ((.) \circ F) \subseteq ℝ$
91		ovolss	$⊢ (⋃_{x = 1}^{n} ((.) \circ F) (x) \subseteq ⋃ ran ((.) \circ F) \land ⋃ ran ((.) \circ F) \subseteq ℝ) \to {vol}^{} (⋃_{x = 1}^{n} ((.) \circ F) (x)) \leq {vol}^{} (⋃ ran ((.) \circ F))$
92	89 90 91	syl2anc	$⊢ (φ \land n \in ℕ) \to {vol}^{} (⋃_{x = 1}^{n} ((.) \circ F) (x)) \leq {vol}^{} (⋃ ran ((.) \circ F))$
93	82 92	eqbrtrd	$⊢ (φ \land n \in ℕ) \to S (n) \leq {vol}^{*} (⋃ ran ((.) \circ F))$
94	93	ralrimiva	$⊢ φ \to \forall n \in ℕ S (n) \leq {vol}^{*} (⋃ ran ((.) \circ F))$
95	1 18	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
96		ffn	$⊢ S : ℕ ⟶ [0, +∞) \to S Fn ℕ$
97		breq1	$⊢ y = S (n) \to (y \leq {vol}^{} (⋃ ran ((.) \circ F)) \leftrightarrow S (n) \leq {vol}^{} (⋃ ran ((.) \circ F)))$
98	97	ralrn	$⊢ S Fn ℕ \to (\forall y \in ran S y \leq {vol}^{} (⋃ ran ((.) \circ F)) \leftrightarrow \forall n \in ℕ S (n) \leq {vol}^{} (⋃ ran ((.) \circ F)))$
99	95 96 98	3syl	$⊢ φ \to (\forall y \in ran S y \leq {vol}^{} (⋃ ran ((.) \circ F)) \leftrightarrow \forall n \in ℕ S (n) \leq {vol}^{} (⋃ ran ((.) \circ F)))$
100	94 99	mpbird	$⊢ φ \to \forall y \in ran S y \leq {vol}^{*} (⋃ ran ((.) \circ F))$
101		supxrleub	$⊢ (ran S \subseteq ℝ^{} \land {vol}^{} (⋃ ran ((.) \circ F)) \in ℝ^{}) \to (sup (ran S ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ F)) \leftrightarrow \forall y \in ran S y \leq {vol}^{} (⋃ ran ((.) \circ F)))$
102	22 16 101	syl2anc	$⊢ φ \to (sup (ran S ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ F)) \leftrightarrow \forall y \in ran S y \leq {vol}^{*} (⋃ ran ((.) \circ F)))$
103	100 102	mpbird	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ F))$
104	16 24 27 103	xrletrid	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ F)) = sup (ran S ℝ^{} <)$

Metamath Proof Explorer

Theorem uniioovol

Proof