Theorem voliunlem2

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

	Ref	Expression
Hypotheses	voliunlem.3	$$⊢\phi \to F:\mathbb{N}⟶\mathrm{dom}vol$$
	voliunlem.5	$$⊢\phi \to \underset{i\in \mathbb{N}}{Disj}F\left(i\right)$$
	voliunlem.6	$$⊢H=\left(n\in \mathbb{N}⟼{vol}^{*}\left(x\cap F\left(n\right)\right)\right)$$
Assertion	voliunlem2	$$⊢\phi \to \bigcup \mathrm{ran}F\in \mathrm{dom}vol$$

Proof

Step	Hyp	Ref	Expression
1		voliunlem.3	$$⊢\phi \to F:\mathbb{N}⟶\mathrm{dom}vol$$
2		voliunlem.5	$$⊢\phi \to \underset{i\in \mathbb{N}}{Disj}F\left(i\right)$$
3		voliunlem.6	$$⊢H=\left(n\in \mathbb{N}⟼{vol}^{*}\left(x\cap F\left(n\right)\right)\right)$$
4	1	frnd	$$⊢\phi \to \mathrm{ran}F\subseteq \mathrm{dom}vol$$
5		mblss	$$⊢x\in \mathrm{dom}vol\to x\subseteq ℝ$$
6		velpw	$$⊢x\in 𝒫ℝ\leftrightarrow x\subseteq ℝ$$
7	5 6	sylibr	$$⊢x\in \mathrm{dom}vol\to x\in 𝒫ℝ$$
8	7	ssriv	$$⊢\mathrm{dom}vol\subseteq 𝒫ℝ$$
9	4 8	sstrdi	$$⊢\phi \to \mathrm{ran}F\subseteq 𝒫ℝ$$
10		sspwuni	$$⊢\mathrm{ran}F\subseteq 𝒫ℝ\leftrightarrow \bigcup \mathrm{ran}F\subseteq ℝ$$
11	9 10	sylib	$$⊢\phi \to \bigcup \mathrm{ran}F\subseteq ℝ$$
12		elpwi	$$⊢x\in 𝒫ℝ\to x\subseteq ℝ$$
13		inundif	$$⊢\left(x\cap \bigcup \mathrm{ran}F\right)\cup \left(x\setminus \bigcup \mathrm{ran}F\right)=x$$
14	13	fveq2i	$$⊢{vol}^{*}\left(\left(x\cap \bigcup \mathrm{ran}F\right)\cup \left(x\setminus \bigcup \mathrm{ran}F\right)\right)={vol}^{*}\left(x\right)$$
15		inss1	$$⊢x\cap \bigcup \mathrm{ran}F\subseteq x$$
16		simp2	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\subseteq ℝ$$
17	15 16	sstrid	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\cap \bigcup \mathrm{ran}F\subseteq ℝ$$
18		ovolsscl	$$⊢\left(x\cap \bigcup \mathrm{ran}F\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\in ℝ$$
19	15 18	mp3an1	$$⊢\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\in ℝ$$
20	19	3adant1	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\in ℝ$$
21		difss	$$⊢x\setminus \bigcup \mathrm{ran}F\subseteq x$$
22	21 16	sstrid	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\setminus \bigcup \mathrm{ran}F\subseteq ℝ$$
23		ovolsscl	$$⊢\left(x\setminus \bigcup \mathrm{ran}F\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ$$
24	21 23	mp3an1	$$⊢\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ$$
25	24	3adant1	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ$$
26		ovolun	$$⊢\left(\left(x\cap \bigcup \mathrm{ran}F\subseteq ℝ\wedge {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\in ℝ\right)\wedge \left(x\setminus \bigcup \mathrm{ran}F\subseteq ℝ\wedge {vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left(x\cap \bigcup \mathrm{ran}F\right)\cup \left(x\setminus \bigcup \mathrm{ran}F\right)\right)\le {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
27	17 20 22 25 26	syl22anc	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(\left(x\cap \bigcup \mathrm{ran}F\right)\cup \left(x\setminus \bigcup \mathrm{ran}F\right)\right)\le {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
28	14 27	eqbrtrrid	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)\le {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
29	20	rexrd	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\in {ℝ}^{*}$$
30		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
31		1zzd	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to 1\in \mathbb{Z}$$
32		fveq2	$$⊢n=k\to F\left(n\right)=F\left(k\right)$$
33	32	ineq2d	$$⊢n=k\to x\cap F\left(n\right)=x\cap F\left(k\right)$$
34	33	fveq2d	$$⊢n=k\to {vol}^{*}\left(x\cap F\left(n\right)\right)={vol}^{*}\left(x\cap F\left(k\right)\right)$$
35		fvex	$$⊢{vol}^{*}\left(x\cap F\left(k\right)\right)\in \mathrm{V}$$
36	34 3 35	fvmpt	$$⊢k\in \mathbb{N}\to H\left(k\right)={vol}^{*}\left(x\cap F\left(k\right)\right)$$
37	36	adantl	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to H\left(k\right)={vol}^{*}\left(x\cap F\left(k\right)\right)$$
38		inss1	$$⊢x\cap F\left(k\right)\subseteq x$$
39		ovolsscl	$$⊢\left(x\cap F\left(k\right)\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap F\left(k\right)\right)\in ℝ$$
40	38 39	mp3an1	$$⊢\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap F\left(k\right)\right)\in ℝ$$
41	40	3adant1	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap F\left(k\right)\right)\in ℝ$$
42	41	adantr	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to {vol}^{*}\left(x\cap F\left(k\right)\right)\in ℝ$$
43	37 42	eqeltrd	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to H\left(k\right)\in ℝ$$
44	30 31 43	serfre	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to seq1\left(+,H\right):\mathbb{N}⟶ℝ$$
45	44	frnd	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \mathrm{ran}seq1\left(+,H\right)\subseteq ℝ$$
46		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
47	45 46	sstrdi	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \mathrm{ran}seq1\left(+,H\right)\subseteq {ℝ}^{*}$$
48		supxrcl	$$⊢\mathrm{ran}seq1\left(+,H\right)\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}seq1\left(+,H\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$$
49	47 48	syl	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to sup\left(\mathrm{ran}seq1\left(+,H\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$$
50		simp3	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)\in ℝ$$
51	50 25	resubcld	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ$$
52	51	rexrd	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in {ℝ}^{*}$$
53		iunin2	$$⊢\bigcup _{n\in \mathbb{N}}\left(x\cap F\left(n\right)\right)=x\cap \bigcup _{n\in \mathbb{N}}F\left(n\right)$$
54		ffn	$$⊢F:\mathbb{N}⟶\mathrm{dom}vol\to FFn\mathbb{N}$$
55		fniunfv	$$⊢FFn\mathbb{N}\to \bigcup _{n\in \mathbb{N}}F\left(n\right)=\bigcup \mathrm{ran}F$$
56	1 54 55	3syl	$$⊢\phi \to \bigcup _{n\in \mathbb{N}}F\left(n\right)=\bigcup \mathrm{ran}F$$
57	56	3ad2ant1	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \bigcup _{n\in \mathbb{N}}F\left(n\right)=\bigcup \mathrm{ran}F$$
58	57	ineq2d	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\cap \bigcup _{n\in \mathbb{N}}F\left(n\right)=x\cap \bigcup \mathrm{ran}F$$
59	53 58	eqtrid	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \bigcup _{n\in \mathbb{N}}\left(x\cap F\left(n\right)\right)=x\cap \bigcup \mathrm{ran}F$$
60	59	fveq2d	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup _{n\in \mathbb{N}}\left(x\cap F\left(n\right)\right)\right)={vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)$$
61		eqid	$$⊢seq1\left(+,H\right)=seq1\left(+,H\right)$$
62		inss1	$$⊢x\cap F\left(n\right)\subseteq x$$
63	62 16	sstrid	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\cap F\left(n\right)\subseteq ℝ$$
64	63	adantr	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge n\in \mathbb{N}\right)\to x\cap F\left(n\right)\subseteq ℝ$$
65		ovolsscl	$$⊢\left(x\cap F\left(n\right)\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap F\left(n\right)\right)\in ℝ$$
66	62 65	mp3an1	$$⊢\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap F\left(n\right)\right)\in ℝ$$
67	66	3adant1	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap F\left(n\right)\right)\in ℝ$$
68	67	adantr	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge n\in \mathbb{N}\right)\to {vol}^{*}\left(x\cap F\left(n\right)\right)\in ℝ$$
69	61 3 64 68	ovoliun	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup _{n\in \mathbb{N}}\left(x\cap F\left(n\right)\right)\right)\le sup\left(\mathrm{ran}seq1\left(+,H\right),{ℝ}^{*},<\right)$$
70	60 69	eqbrtrrd	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\le sup\left(\mathrm{ran}seq1\left(+,H\right),{ℝ}^{*},<\right)$$
71	1	3ad2ant1	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to F:\mathbb{N}⟶\mathrm{dom}vol$$
72	2	3ad2ant1	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \underset{i\in \mathbb{N}}{Disj}F\left(i\right)$$
73	71 72 3 16 50	voliunlem1	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to seq1\left(+,H\right)\left(k\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)$$
74	44	ffvelcdmda	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to seq1\left(+,H\right)\left(k\right)\in ℝ$$
75	25	adantr	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to {vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ$$
76		simpl3	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to {vol}^{*}\left(x\right)\in ℝ$$
77		leaddsub	$$⊢\left(seq1\left(+,H\right)\left(k\right)\in ℝ\wedge {vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \left(seq1\left(+,H\right)\left(k\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)\leftrightarrow seq1\left(+,H\right)\left(k\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
78	74 75 76 77	syl3anc	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to \left(seq1\left(+,H\right)\left(k\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)\leftrightarrow seq1\left(+,H\right)\left(k\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
79	73 78	mpbid	$$⊢\left(\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\wedge k\in \mathbb{N}\right)\to seq1\left(+,H\right)\left(k\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
80	79	ralrimiva	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \forall k\in \mathbb{N}seq1\left(+,H\right)\left(k\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
81		ffn	$$⊢seq1\left(+,H\right):\mathbb{N}⟶ℝ\to seq1\left(+,H\right)Fn\mathbb{N}$$
82		breq1	$$⊢z=seq1\left(+,H\right)\left(k\right)\to \left(z\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\leftrightarrow seq1\left(+,H\right)\left(k\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
83	82	ralrn	$$⊢seq1\left(+,H\right)Fn\mathbb{N}\to \left(\forall z\in \mathrm{ran}seq1\left(+,H\right)z\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\leftrightarrow \forall k\in \mathbb{N}seq1\left(+,H\right)\left(k\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
84	44 81 83	3syl	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \left(\forall z\in \mathrm{ran}seq1\left(+,H\right)z\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\leftrightarrow \forall k\in \mathbb{N}seq1\left(+,H\right)\left(k\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
85	80 84	mpbird	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \forall z\in \mathrm{ran}seq1\left(+,H\right)z\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
86		supxrleub	$$⊢\left(\mathrm{ran}seq1\left(+,H\right)\subseteq {ℝ}^{*}\wedge {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}seq1\left(+,H\right),{ℝ}^{*},<\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\leftrightarrow \forall z\in \mathrm{ran}seq1\left(+,H\right)z\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
87	47 52 86	syl2anc	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \left(sup\left(\mathrm{ran}seq1\left(+,H\right),{ℝ}^{*},<\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\leftrightarrow \forall z\in \mathrm{ran}seq1\left(+,H\right)z\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
88	85 87	mpbird	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to sup\left(\mathrm{ran}seq1\left(+,H\right),{ℝ}^{*},<\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
89	29 49 52 70 88	xrletrd	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
90		leaddsub	$$⊢\left({vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\in ℝ\wedge {vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \left({vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)\leftrightarrow {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
91	20 25 50 90	syl3anc	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \left({vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)\leftrightarrow {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)-{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
92	89 91	mpbird	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)$$
93	20 25	readdcld	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\in ℝ$$
94	50 93	letri3d	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to \left({vol}^{*}\left(x\right)={vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\leftrightarrow \left({vol}^{*}\left(x\right)\le {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\wedge {vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\le {vol}^{*}\left(x\right)\right)\right)$$
95	28 92 94	mpbir2and	$$⊢\left(\phi \wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)$$
96	95	3expia	$$⊢\left(\phi \wedge x\subseteq ℝ\right)\to \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
97	12 96	sylan2	$$⊢\left(\phi \wedge x\in 𝒫ℝ\right)\to \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
98	97	ralrimiva	$$⊢\phi \to \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)$$
99		ismbl	$$⊢\bigcup \mathrm{ran}F\in \mathrm{dom}vol\leftrightarrow \left(\bigcup \mathrm{ran}F\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap \bigcup \mathrm{ran}F\right)+{vol}^{*}\left(x\setminus \bigcup \mathrm{ran}F\right)\right)\right)$$
100	11 98 99	sylanbrc	$$⊢\phi \to \bigcup \mathrm{ran}F\in \mathrm{dom}vol$$