volsup

Description: The volume of the limit of an increasing sequence of measurable sets is the limit of the volumes. (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 11-Dec-2016)

		Ref	Expression
	Assertion	volsup	$⊢ (F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \to vol (⋃ ran F) = sup (vol [ran F] ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		ffvelcdm	$⊢ (F : ℕ ⟶ dom vol \land k \in ℕ) \to F (k) \in dom vol$
2	1	ad2ant2r	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to F (k) \in dom vol$
3		fzofi	$⊢ (1 ..^k) \in Fin$
4		simpll	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to F : ℕ ⟶ dom vol$
5		elfzouz	$⊢ m \in (1 ..^k) \to m \in ℤ_{\geq 1}$
6		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
7	5 6	eleqtrrdi	$⊢ m \in (1 ..^k) \to m \in ℕ$
8		ffvelcdm	$⊢ (F : ℕ ⟶ dom vol \land m \in ℕ) \to F (m) \in dom vol$
9	4 7 8	syl2an	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \land m \in (1 ..^k)) \to F (m) \in dom vol$
10	9	ralrimiva	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to \forall m \in (1 ..^k) F (m) \in dom vol$
11		finiunmbl	$⊢ ((1 ..^k) \in Fin \land \forall m \in (1 ..^k) F (m) \in dom vol) \to ⋃_{m \in (1 ..^k)} F (m) \in dom vol$
12	3 10 11	sylancr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to ⋃_{m \in (1 ..^k)} F (m) \in dom vol$
13		difmbl	$⊢ (F (k) \in dom vol \land ⋃_{m \in (1 ..^k)} F (m) \in dom vol) \to F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol$
14	2 12 13	syl2anc	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol$
15		mblvol	$⊢ F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol \to vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) = {vol}^{*} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))$
16	14 15	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) = {vol}^{*} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))$
17		difssd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \subseteq F (k)$
18		mblss	$⊢ F (k) \in dom vol \to F (k) \subseteq ℝ$
19	2 18	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to F (k) \subseteq ℝ$
20		mblvol	$⊢ F (k) \in dom vol \to vol (F (k)) = {vol}^{*} (F (k))$
21	2 20	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to vol (F (k)) = {vol}^{*} (F (k))$
22		simprr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to vol (F (k)) \in ℝ$
23	21 22	eqeltrrd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to {vol}^{*} (F (k)) \in ℝ$
24		ovolsscl	$⊢ (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \subseteq F (k) \land F (k) \subseteq ℝ \land {vol}^{} (F (k)) \in ℝ) \to {vol}^{} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ$
25	17 19 23 24	syl3anc	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to {vol}^{*} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ$
26	16 25	eqeltrd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ$
27	14 26	jca	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land vol (F (k)) \in ℝ)) \to (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol \land vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ)$
28	27	expr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land k \in ℕ) \to (vol (F (k)) \in ℝ \to (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol \land vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ))$
29	28	ralimdva	$⊢ (F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \to (\forall k \in ℕ vol (F (k)) \in ℝ \to \forall k \in ℕ (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol \land vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ))$
30	29	imp	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to \forall k \in ℕ (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol \land vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ)$
31		fveq2	$⊢ k = m \to F (k) = F (m)$
32	31	iundisj2	$⊢ \underset{k \in ℕ}{Disj} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))$
33		eqid	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) = seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))))$
34		eqid	$⊢ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) = (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))$
35	33 34	voliun	$⊢ (\forall k \in ℕ (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) \in dom vol \land vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) \in ℝ) \land \underset{k \in ℕ}{Disj} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) \to vol (⋃_{k \in ℕ} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) = sup (ran seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) ℝ^{*} <)$
36	30 32 35	sylancl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to vol (⋃_{k \in ℕ} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) = sup (ran seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) ℝ^{*} <)$
37	31	iundisj	$⊢ ⋃_{k \in ℕ} F (k) = ⋃_{k \in ℕ} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))$
38		ffn	$⊢ F : ℕ ⟶ dom vol \to F Fn ℕ$
39	38	ad2antrr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to F Fn ℕ$
40		fniunfv	$⊢ F Fn ℕ \to ⋃_{k \in ℕ} F (k) = ⋃ ran F$
41	39 40	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to ⋃_{k \in ℕ} F (k) = ⋃ ran F$
42	37 41	eqtr3id	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to ⋃_{k \in ℕ} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) = ⋃ ran F$
43	42	fveq2d	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to vol (⋃_{k \in ℕ} (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) = vol (⋃ ran F)$
44		1z	$⊢ 1 \in ℤ$
45		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) Fn ℤ_{\geq 1}$
46	44 45	ax-mp	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) Fn ℤ_{\geq 1}$
47	6	fneq2i	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) Fn ℕ \leftrightarrow seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) Fn ℤ_{\geq 1}$
48	46 47	mpbir	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) Fn ℕ$
49	48	a1i	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) Fn ℕ$
50		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
51		simpll	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to F : ℕ ⟶ dom vol$
52		fco	$⊢ (vol : dom vol ⟶ [0, +∞] \land F : ℕ ⟶ dom vol) \to (vol \circ F) : ℕ ⟶ [0, +∞]$
53	50 51 52	sylancr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to (vol \circ F) : ℕ ⟶ [0, +∞]$
54	53	ffnd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to (vol \circ F) Fn ℕ$
55		fveq2	$⊢ x = 1 \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (1)$
56		2fveq3	$⊢ x = 1 \to vol (F (x)) = vol (F (1))$
57	55 56	eqeq12d	$⊢ x = 1 \to (seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = vol (F (x)) \leftrightarrow seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (1) = vol (F (1)))$
58	57	imbi2d	$⊢ x = 1 \to ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = vol (F (x))) \leftrightarrow (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (1) = vol (F (1))))$
59		fveq2	$⊢ x = j \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j)$
60		2fveq3	$⊢ x = j \to vol (F (x)) = vol (F (j))$
61	59 60	eqeq12d	$⊢ x = j \to (seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = vol (F (x)) \leftrightarrow seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j)))$
62	61	imbi2d	$⊢ x = j \to ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = vol (F (x))) \leftrightarrow (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j))))$
63		fveq2	$⊢ x = j + 1 \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1)$
64		2fveq3	$⊢ x = j + 1 \to vol (F (x)) = vol (F (j + 1))$
65	63 64	eqeq12d	$⊢ x = j + 1 \to (seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = vol (F (x)) \leftrightarrow seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = vol (F (j + 1)))$
66	65	imbi2d	$⊢ x = j + 1 \to ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (x) = vol (F (x))) \leftrightarrow (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = vol (F (j + 1))))$
67		seq1	$⊢ 1 \in ℤ \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (1) = (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (1)$
68	44 67	ax-mp	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (1) = (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (1)$
69		1nn	$⊢ 1 \in ℕ$
70		oveq2	$⊢ k = 1 \to (1 ..^k) = (1 ..^1)$
71		fzo0	$⊢ (1 ..^1) = \emptyset$
72	70 71	eqtrdi	$⊢ k = 1 \to (1 ..^k) = \emptyset$
73	72	iuneq1d	$⊢ k = 1 \to ⋃_{m \in (1 ..^k)} F (m) = ⋃_{m \in \emptyset} F (m)$
74		0iun	$⊢ ⋃_{m \in \emptyset} F (m) = \emptyset$
75	73 74	eqtrdi	$⊢ k = 1 \to ⋃_{m \in (1 ..^k)} F (m) = \emptyset$
76	75	difeq2d	$⊢ k = 1 \to F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) = F (k) ∖ \emptyset$
77		dif0	$⊢ F (k) ∖ \emptyset = F (k)$
78	76 77	eqtrdi	$⊢ k = 1 \to F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) = F (k)$
79		fveq2	$⊢ k = 1 \to F (k) = F (1)$
80	78 79	eqtrd	$⊢ k = 1 \to F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) = F (1)$
81	80	fveq2d	$⊢ k = 1 \to vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) = vol (F (1))$
82		fvex	$⊢ vol (F (1)) \in V$
83	81 34 82	fvmpt	$⊢ 1 \in ℕ \to (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (1) = vol (F (1))$
84	69 83	ax-mp	$⊢ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (1) = vol (F (1))$
85	68 84	eqtri	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (1) = vol (F (1))$
86	85	a1i	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (1) = vol (F (1))$
87		oveq1	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j)) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1) = vol (F (j)) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1)$
88		seqp1	$⊢ j \in ℤ_{\geq 1} \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1)$
89	88 6	eleq2s	$⊢ j \in ℕ \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1)$
90	89	adantl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1)$
91		undif2	$⊢ F (j) \cup (F (j + 1) ∖ F (j)) = F (j) \cup F (j + 1)$
92		fveq2	$⊢ n = j \to F (n) = F (j)$
93		fvoveq1	$⊢ n = j \to F (n + 1) = F (j + 1)$
94	92 93	sseq12d	$⊢ n = j \to (F (n) \subseteq F (n + 1) \leftrightarrow F (j) \subseteq F (j + 1))$
95		simpllr	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to \forall n \in ℕ F (n) \subseteq F (n + 1)$
96		simpr	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to j \in ℕ$
97	94 95 96	rspcdva	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j) \subseteq F (j + 1)$
98		ssequn1	$⊢ F (j) \subseteq F (j + 1) \leftrightarrow F (j) \cup F (j + 1) = F (j + 1)$
99	97 98	sylib	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j) \cup F (j + 1) = F (j + 1)$
100	91 99	eqtr2id	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j + 1) = F (j) \cup (F (j + 1) ∖ F (j))$
101	100	fveq2d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1)) = vol (F (j) \cup (F (j + 1) ∖ F (j)))$
102		simplll	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F : ℕ ⟶ dom vol$
103	102 96	ffvelcdmd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j) \in dom vol$
104		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
105	104	adantl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to j + 1 \in ℕ$
106	102 105	ffvelcdmd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j + 1) \in dom vol$
107		difmbl	$⊢ (F (j + 1) \in dom vol \land F (j) \in dom vol) \to F (j + 1) ∖ F (j) \in dom vol$
108	106 103 107	syl2anc	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j + 1) ∖ F (j) \in dom vol$
109		disjdif	$⊢ F (j) \cap (F (j + 1) ∖ F (j)) = \emptyset$
110	109	a1i	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j) \cap (F (j + 1) ∖ F (j)) = \emptyset$
111		2fveq3	$⊢ k = j \to vol (F (k)) = vol (F (j))$
112	111	eleq1d	$⊢ k = j \to (vol (F (k)) \in ℝ \leftrightarrow vol (F (j)) \in ℝ)$
113		simplr	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to \forall k \in ℕ vol (F (k)) \in ℝ$
114	112 113 96	rspcdva	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j)) \in ℝ$
115		mblvol	$⊢ F (j + 1) ∖ F (j) \in dom vol \to vol (F (j + 1) ∖ F (j)) = {vol}^{*} (F (j + 1) ∖ F (j))$
116	108 115	syl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1) ∖ F (j)) = {vol}^{*} (F (j + 1) ∖ F (j))$
117		difssd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j + 1) ∖ F (j) \subseteq F (j + 1)$
118		mblss	$⊢ F (j + 1) \in dom vol \to F (j + 1) \subseteq ℝ$
119	106 118	syl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j + 1) \subseteq ℝ$
120		mblvol	$⊢ F (j + 1) \in dom vol \to vol (F (j + 1)) = {vol}^{*} (F (j + 1))$
121	106 120	syl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1)) = {vol}^{*} (F (j + 1))$
122		2fveq3	$⊢ k = j + 1 \to vol (F (k)) = vol (F (j + 1))$
123	122	eleq1d	$⊢ k = j + 1 \to (vol (F (k)) \in ℝ \leftrightarrow vol (F (j + 1)) \in ℝ)$
124	123 113 105	rspcdva	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1)) \in ℝ$
125	121 124	eqeltrrd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to {vol}^{*} (F (j + 1)) \in ℝ$
126		ovolsscl	$⊢ (F (j + 1) ∖ F (j) \subseteq F (j + 1) \land F (j + 1) \subseteq ℝ \land {vol}^{} (F (j + 1)) \in ℝ) \to {vol}^{} (F (j + 1) ∖ F (j)) \in ℝ$
127	117 119 125 126	syl3anc	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to {vol}^{*} (F (j + 1) ∖ F (j)) \in ℝ$
128	116 127	eqeltrd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1) ∖ F (j)) \in ℝ$
129		volun	$⊢ ((F (j) \in dom vol \land F (j + 1) ∖ F (j) \in dom vol \land F (j) \cap (F (j + 1) ∖ F (j)) = \emptyset) \land (vol (F (j)) \in ℝ \land vol (F (j + 1) ∖ F (j)) \in ℝ)) \to vol (F (j) \cup (F (j + 1) ∖ F (j))) = vol (F (j)) + vol (F (j + 1) ∖ F (j))$
130	103 108 110 114 128 129	syl32anc	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j) \cup (F (j + 1) ∖ F (j))) = vol (F (j)) + vol (F (j + 1) ∖ F (j))$
131	95	adantr	$⊢ ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \land m \in (1 \dots j)) \to \forall n \in ℕ F (n) \subseteq F (n + 1)$
132		elfznn	$⊢ m \in (1 \dots j) \to m \in ℕ$
133	132	adantl	$⊢ ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \land m \in (1 \dots j)) \to m \in ℕ$
134		elfzuz3	$⊢ m \in (1 \dots j) \to j \in ℤ_{\geq m}$
135	134	adantl	$⊢ ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \land m \in (1 \dots j)) \to j \in ℤ_{\geq m}$
136		volsuplem	$⊢ (\forall n \in ℕ F (n) \subseteq F (n + 1) \land (m \in ℕ \land j \in ℤ_{\geq m})) \to F (m) \subseteq F (j)$
137	131 133 135 136	syl12anc	$⊢ ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \land m \in (1 \dots j)) \to F (m) \subseteq F (j)$
138	137	ralrimiva	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to \forall m \in (1 \dots j) F (m) \subseteq F (j)$
139		iunss	$⊢ ⋃_{m = 1}^{j} F (m) \subseteq F (j) \leftrightarrow \forall m \in (1 \dots j) F (m) \subseteq F (j)$
140	138 139	sylibr	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to ⋃_{m = 1}^{j} F (m) \subseteq F (j)$
141	96 6	eleqtrdi	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to j \in ℤ_{\geq 1}$
142		eluzfz2	$⊢ j \in ℤ_{\geq 1} \to j \in (1 \dots j)$
143	141 142	syl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to j \in (1 \dots j)$
144		fveq2	$⊢ m = j \to F (m) = F (j)$
145	144	ssiun2s	$⊢ j \in (1 \dots j) \to F (j) \subseteq ⋃_{m = 1}^{j} F (m)$
146	143 145	syl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j) \subseteq ⋃_{m = 1}^{j} F (m)$
147	140 146	eqssd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to ⋃_{m = 1}^{j} F (m) = F (j)$
148	96	nnzd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to j \in ℤ$
149		fzval3	$⊢ j \in ℤ \to (1 \dots j) = (1 ..^j + 1)$
150	148 149	syl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to (1 \dots j) = (1 ..^j + 1)$
151	150	iuneq1d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to ⋃_{m = 1}^{j} F (m) = ⋃_{m \in (1 ..^j + 1)} F (m)$
152	147 151	eqtr3d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j) = ⋃_{m \in (1 ..^j + 1)} F (m)$
153	152	difeq2d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to F (j + 1) ∖ F (j) = F (j + 1) ∖ ⋃_{m \in (1 ..^j + 1)} F (m)$
154	153	fveq2d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1) ∖ F (j)) = vol (F (j + 1) ∖ ⋃_{m \in (1 ..^j + 1)} F (m))$
155		fveq2	$⊢ k = j + 1 \to F (k) = F (j + 1)$
156		oveq2	$⊢ k = j + 1 \to (1 ..^k) = (1 ..^j + 1)$
157	156	iuneq1d	$⊢ k = j + 1 \to ⋃_{m \in (1 ..^k)} F (m) = ⋃_{m \in (1 ..^j + 1)} F (m)$
158	155 157	difeq12d	$⊢ k = j + 1 \to F (k) ∖ ⋃_{m \in (1 ..^k)} F (m) = F (j + 1) ∖ ⋃_{m \in (1 ..^j + 1)} F (m)$
159	158	fveq2d	$⊢ k = j + 1 \to vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)) = vol (F (j + 1) ∖ ⋃_{m \in (1 ..^j + 1)} F (m))$
160		fvex	$⊢ vol (F (j + 1) ∖ ⋃_{m \in (1 ..^j + 1)} F (m)) \in V$
161	159 34 160	fvmpt	$⊢ j + 1 \in ℕ \to (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1) = vol (F (j + 1) ∖ ⋃_{m \in (1 ..^j + 1)} F (m))$
162	105 161	syl	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1) = vol (F (j + 1) ∖ ⋃_{m \in (1 ..^j + 1)} F (m))$
163	154 162	eqtr4d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1) ∖ F (j)) = (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1)$
164	163	oveq2d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j)) + vol (F (j + 1) ∖ F (j)) = vol (F (j)) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1)$
165	101 130 164	3eqtrd	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to vol (F (j + 1)) = vol (F (j)) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1)$
166	90 165	eqeq12d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to (seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = vol (F (j + 1)) \leftrightarrow seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1) = vol (F (j)) + (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m))) (j + 1))$
167	87 166	imbitrrid	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to (seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j)) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = vol (F (j + 1)))$
168	167	expcom	$⊢ j \in ℕ \to (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to (seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j)) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = vol (F (j + 1))))$
169	168	a2d	$⊢ j \in ℕ \to ((((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j))) \to (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j + 1) = vol (F (j + 1))))$
170	58 62 66 62 86 169	nnind	$⊢ j \in ℕ \to (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j)))$
171	170	impcom	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = vol (F (j))$
172		fvco3	$⊢ (F : ℕ ⟶ dom vol \land j \in ℕ) \to (vol \circ F) (j) = vol (F (j))$
173	51 172	sylan	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to (vol \circ F) (j) = vol (F (j))$
174	171 173	eqtr4d	$⊢ (((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \land j \in ℕ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) (j) = (vol \circ F) (j)$
175	49 54 174	eqfnfvd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) = vol \circ F$
176	175	rneqd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to ran seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) = ran (vol \circ F)$
177		rnco2	$⊢ ran (vol \circ F) = vol [ran F]$
178	176 177	eqtrdi	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to ran seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) = vol [ran F]$
179	178	supeq1d	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to sup (ran seq 1 (+ (k \in ℕ ⟼ vol (F (k) ∖ ⋃_{m \in (1 ..^k)} F (m)))) ℝ^{} <) = sup (vol [ran F] ℝ^{} <)$
180	36 43 179	3eqtr3d	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land \forall k \in ℕ vol (F (k)) \in ℝ) \to vol (⋃ ran F) = sup (vol [ran F] ℝ^{*} <)$
181	180	ex	$⊢ (F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \to (\forall k \in ℕ vol (F (k)) \in ℝ \to vol (⋃ ran F) = sup (vol [ran F] ℝ^{*} <))$
182		rexnal	$⊢ \exists k \in ℕ \neg vol (F (k)) \in ℝ \leftrightarrow \neg \forall k \in ℕ vol (F (k)) \in ℝ$
183		fniunfv	$⊢ F Fn ℕ \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
184	38 183	syl	$⊢ F : ℕ ⟶ dom vol \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
185		ffvelcdm	$⊢ (F : ℕ ⟶ dom vol \land n \in ℕ) \to F (n) \in dom vol$
186	185	ralrimiva	$⊢ F : ℕ ⟶ dom vol \to \forall n \in ℕ F (n) \in dom vol$
187		iunmbl	$⊢ \forall n \in ℕ F (n) \in dom vol \to ⋃_{n \in ℕ} F (n) \in dom vol$
188	186 187	syl	$⊢ F : ℕ ⟶ dom vol \to ⋃_{n \in ℕ} F (n) \in dom vol$
189	184 188	eqeltrrd	$⊢ F : ℕ ⟶ dom vol \to ⋃ ran F \in dom vol$
190	189	ad2antrr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to ⋃ ran F \in dom vol$
191		mblss	$⊢ ⋃ ran F \in dom vol \to ⋃ ran F \subseteq ℝ$
192	190 191	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to ⋃ ran F \subseteq ℝ$
193		ovolcl	$⊢ ⋃ ran F \subseteq ℝ \to {vol}^{} (⋃ ran F) \in ℝ^{}$
194	192 193	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to {vol}^{} (⋃ ran F) \in ℝ^{}$
195		pnfge	$⊢ {vol}^{} (⋃ ran F) \in ℝ^{} \to {vol}^{*} (⋃ ran F) \leq +∞$
196	194 195	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to {vol}^{*} (⋃ ran F) \leq +∞$
197		simprr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to \neg vol (F (k)) \in ℝ$
198	1	ad2ant2r	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to F (k) \in dom vol$
199	198 18	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to F (k) \subseteq ℝ$
200		ovolcl	$⊢ F (k) \subseteq ℝ \to {vol}^{} (F (k)) \in ℝ^{}$
201	199 200	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to {vol}^{} (F (k)) \in ℝ^{}$
202		xrrebnd	$⊢ {vol}^{} (F (k)) \in ℝ^{} \to ({vol}^{} (F (k)) \in ℝ \leftrightarrow (−∞ < {vol}^{} (F (k)) \land {vol}^{*} (F (k)) < +∞))$
203	201 202	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to ({vol}^{} (F (k)) \in ℝ \leftrightarrow (−∞ < {vol}^{} (F (k)) \land {vol}^{*} (F (k)) < +∞))$
204	198 20	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to vol (F (k)) = {vol}^{*} (F (k))$
205	204	eleq1d	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to (vol (F (k)) \in ℝ \leftrightarrow {vol}^{*} (F (k)) \in ℝ)$
206		ovolge0	$⊢ F (k) \subseteq ℝ \to 0 \leq {vol}^{*} (F (k))$
207		mnflt0	$⊢ −∞ < 0$
208		mnfxr	$⊢ −∞ \in ℝ^{*}$
209		0xr	$⊢ 0 \in ℝ^{*}$
210		xrltletr	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land {vol}^{} (F (k)) \in ℝ^{}) \to ((−∞ < 0 \land 0 \leq {vol}^{} (F (k))) \to −∞ < {vol}^{} (F (k)))$
211	208 209 210	mp3an12	$⊢ {vol}^{} (F (k)) \in ℝ^{} \to ((−∞ < 0 \land 0 \leq {vol}^{} (F (k))) \to −∞ < {vol}^{} (F (k)))$
212	207 211	mpani	$⊢ {vol}^{} (F (k)) \in ℝ^{} \to (0 \leq {vol}^{} (F (k)) \to −∞ < {vol}^{} (F (k)))$
213	200 206 212	sylc	$⊢ F (k) \subseteq ℝ \to −∞ < {vol}^{*} (F (k))$
214	199 213	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to −∞ < {vol}^{*} (F (k))$
215	214	biantrurd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to ({vol}^{} (F (k)) < +∞ \leftrightarrow (−∞ < {vol}^{} (F (k)) \land {vol}^{*} (F (k)) < +∞))$
216	203 205 215	3bitr4d	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to (vol (F (k)) \in ℝ \leftrightarrow {vol}^{*} (F (k)) < +∞)$
217	197 216	mtbid	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to \neg {vol}^{*} (F (k)) < +∞$
218		nltpnft	$⊢ {vol}^{} (F (k)) \in ℝ^{} \to ({vol}^{} (F (k)) = +∞ \leftrightarrow \neg {vol}^{} (F (k)) < +∞)$
219	201 218	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to ({vol}^{} (F (k)) = +∞ \leftrightarrow \neg {vol}^{} (F (k)) < +∞)$
220	217 219	mpbird	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to {vol}^{*} (F (k)) = +∞$
221	38	ad2antrr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to F Fn ℕ$
222		simprl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to k \in ℕ$
223		fnfvelrn	$⊢ (F Fn ℕ \land k \in ℕ) \to F (k) \in ran F$
224	221 222 223	syl2anc	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to F (k) \in ran F$
225		elssuni	$⊢ F (k) \in ran F \to F (k) \subseteq ⋃ ran F$
226	224 225	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to F (k) \subseteq ⋃ ran F$
227		ovolss	$⊢ (F (k) \subseteq ⋃ ran F \land ⋃ ran F \subseteq ℝ) \to {vol}^{} (F (k)) \leq {vol}^{} (⋃ ran F)$
228	226 192 227	syl2anc	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to {vol}^{} (F (k)) \leq {vol}^{} (⋃ ran F)$
229	220 228	eqbrtrrd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to +∞ \leq {vol}^{*} (⋃ ran F)$
230		pnfxr	$⊢ +∞ \in ℝ^{*}$
231		xrletri3	$⊢ ({vol}^{} (⋃ ran F) \in ℝ^{} \land +∞ \in ℝ^{}) \to ({vol}^{} (⋃ ran F) = +∞ \leftrightarrow ({vol}^{} (⋃ ran F) \leq +∞ \land +∞ \leq {vol}^{} (⋃ ran F)))$
232	194 230 231	sylancl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to ({vol}^{} (⋃ ran F) = +∞ \leftrightarrow ({vol}^{} (⋃ ran F) \leq +∞ \land +∞ \leq {vol}^{*} (⋃ ran F)))$
233	196 229 232	mpbir2and	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to {vol}^{*} (⋃ ran F) = +∞$
234		mblvol	$⊢ ⋃ ran F \in dom vol \to vol (⋃ ran F) = {vol}^{*} (⋃ ran F)$
235	190 234	syl	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to vol (⋃ ran F) = {vol}^{*} (⋃ ran F)$
236		imassrn	$⊢ vol [ran F] \subseteq ran vol$
237		frn	$⊢ vol : dom vol ⟶ [0, +∞] \to ran vol \subseteq [0, +∞]$
238	50 237	ax-mp	$⊢ ran vol \subseteq [0, +∞]$
239		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
240	238 239	sstri	$⊢ ran vol \subseteq ℝ^{*}$
241	236 240	sstri	$⊢ vol [ran F] \subseteq ℝ^{*}$
242	204 220	eqtrd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to vol (F (k)) = +∞$
243		simpll	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to F : ℕ ⟶ dom vol$
244		ffun	$⊢ vol : dom vol ⟶ [0, +∞] \to Fun vol$
245	50 244	ax-mp	$⊢ Fun vol$
246		frn	$⊢ F : ℕ ⟶ dom vol \to ran F \subseteq dom vol$
247		funfvima2	$⊢ (Fun vol \land ran F \subseteq dom vol) \to (F (k) \in ran F \to vol (F (k)) \in vol [ran F])$
248	245 246 247	sylancr	$⊢ F : ℕ ⟶ dom vol \to (F (k) \in ran F \to vol (F (k)) \in vol [ran F])$
249	243 224 248	sylc	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to vol (F (k)) \in vol [ran F]$
250	242 249	eqeltrrd	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to +∞ \in vol [ran F]$
251		supxrpnf	$⊢ (vol [ran F] \subseteq ℝ^{} \land +∞ \in vol [ran F]) \to sup (vol [ran F] ℝ^{} <) = +∞$
252	241 250 251	sylancr	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to sup (vol [ran F] ℝ^{*} <) = +∞$
253	233 235 252	3eqtr4d	$⊢ ((F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \land (k \in ℕ \land \neg vol (F (k)) \in ℝ)) \to vol (⋃ ran F) = sup (vol [ran F] ℝ^{*} <)$
254	253	rexlimdvaa	$⊢ (F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \to (\exists k \in ℕ \neg vol (F (k)) \in ℝ \to vol (⋃ ran F) = sup (vol [ran F] ℝ^{*} <))$
255	182 254	biimtrrid	$⊢ (F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \to (\neg \forall k \in ℕ vol (F (k)) \in ℝ \to vol (⋃ ran F) = sup (vol [ran F] ℝ^{*} <))$
256	181 255	pm2.61d	$⊢ (F : ℕ ⟶ dom vol \land \forall n \in ℕ F (n) \subseteq F (n + 1)) \to vol (⋃ ran F) = sup (vol [ran F] ℝ^{*} <)$

Metamath Proof Explorer

Theorem volsup

Proof