Theorem ovoliunnfl

Description: ovoliun is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017)

	Ref	Expression
Hypothesis	ovoliunnfl.0	$$⊢\left(fFn\mathbb{N}\wedge \forall n\in \mathbb{N}\left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)\in ℝ\right)\right)\to {vol}^{*}\left(\bigcup _{m\in \mathbb{N}}f\left(m\right)\right)\le sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right),{ℝ}^{*},<\right)$$
Assertion	ovoliunnfl	$$⊢\left(A\preccurlyeq \mathbb{N}\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)\to \bigcup A\ne ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ovoliunnfl.0	$$⊢\left(fFn\mathbb{N}\wedge \forall n\in \mathbb{N}\left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)\in ℝ\right)\right)\to {vol}^{*}\left(\bigcup _{m\in \mathbb{N}}f\left(m\right)\right)\le sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right),{ℝ}^{*},<\right)$$
2		unieq	$$⊢A=\varnothing \to \bigcup A=\bigcup \varnothing$$
3		uni0	$$⊢\bigcup \varnothing =\varnothing$$
4	2 3	eqtrdi	$$⊢A=\varnothing \to \bigcup A=\varnothing$$
5	4	fveq2d	$$⊢A=\varnothing \to {vol}^{*}\left(\bigcup A\right)={vol}^{*}\left(\varnothing \right)$$
6		ovol0	$$⊢{vol}^{*}\left(\varnothing \right)=0$$
7	5 6	eqtr2di	$$⊢A=\varnothing \to 0={vol}^{*}\left(\bigcup A\right)$$
8	7	a1d	$$⊢A=\varnothing \to \left(\left(A\preccurlyeq \mathbb{N}\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to 0={vol}^{*}\left(\bigcup A\right)\right)$$
9		ovolge0	$$⊢\bigcup A\subseteq ℝ\to 0\le {vol}^{*}\left(\bigcup A\right)$$
10	9	ad2antll	$$⊢\left(\left(A\ne \varnothing \wedge A\preccurlyeq \mathbb{N}\right)\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to 0\le {vol}^{*}\left(\bigcup A\right)$$
11		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
12	11	brrelex1i	$$⊢A\preccurlyeq \mathbb{N}\to A\in \mathrm{V}$$
13		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
14	12 13	syl	$$⊢A\preccurlyeq \mathbb{N}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
15	14	biimparc	$$⊢\left(A\ne \varnothing \wedge A\preccurlyeq \mathbb{N}\right)\to \varnothing \prec A$$
16		fodomr	$$⊢\left(\varnothing \prec A\wedge A\preccurlyeq \mathbb{N}\right)\to \exists ff:\mathbb{N}\underset{onto}{⟶}A$$
17	15 16	sylancom	$$⊢\left(A\ne \varnothing \wedge A\preccurlyeq \mathbb{N}\right)\to \exists ff:\mathbb{N}\underset{onto}{⟶}A$$
18		unissb	$$⊢\bigcup A\subseteq ℝ\leftrightarrow \forall x\in Ax\subseteq ℝ$$
19	18	anbi1i	$$⊢\left(\bigcup A\subseteq ℝ\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)\leftrightarrow \left(\forall x\in Ax\subseteq ℝ\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)$$
20		r19.26	$$⊢\forall x\in A\left(x\subseteq ℝ\wedge x\preccurlyeq \mathbb{N}\right)\leftrightarrow \left(\forall x\in Ax\subseteq ℝ\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)$$
21	19 20	bitr4i	$$⊢\left(\bigcup A\subseteq ℝ\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)\leftrightarrow \forall x\in A\left(x\subseteq ℝ\wedge x\preccurlyeq \mathbb{N}\right)$$
22		brdom2	$$⊢x\preccurlyeq \mathbb{N}\leftrightarrow \left(x\prec \mathbb{N}\vee x\approx \mathbb{N}\right)$$
23		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
24		sdomen2	$$⊢\mathbb{N}\approx \mathrm{\omega }\to \left(x\prec \mathbb{N}\leftrightarrow x\prec \mathrm{\omega }\right)$$
25	23 24	ax-mp	$$⊢x\prec \mathbb{N}\leftrightarrow x\prec \mathrm{\omega }$$
26		isfinite	$$⊢x\in \mathrm{Fin}\leftrightarrow x\prec \mathrm{\omega }$$
27	25 26	bitr4i	$$⊢x\prec \mathbb{N}\leftrightarrow x\in \mathrm{Fin}$$
28	27	orbi1i	$$⊢\left(x\prec \mathbb{N}\vee x\approx \mathbb{N}\right)\leftrightarrow \left(x\in \mathrm{Fin}\vee x\approx \mathbb{N}\right)$$
29	22 28	bitri	$$⊢x\preccurlyeq \mathbb{N}\leftrightarrow \left(x\in \mathrm{Fin}\vee x\approx \mathbb{N}\right)$$
30		ovolfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\subseteq ℝ\right)\to {vol}^{*}\left(x\right)=0$$
31	30	expcom	$$⊢x\subseteq ℝ\to \left(x\in \mathrm{Fin}\to {vol}^{*}\left(x\right)=0\right)$$
32		ovolctb	$$⊢\left(x\subseteq ℝ\wedge x\approx \mathbb{N}\right)\to {vol}^{*}\left(x\right)=0$$
33	32	ex	$$⊢x\subseteq ℝ\to \left(x\approx \mathbb{N}\to {vol}^{*}\left(x\right)=0\right)$$
34	31 33	jaod	$$⊢x\subseteq ℝ\to \left(\left(x\in \mathrm{Fin}\vee x\approx \mathbb{N}\right)\to {vol}^{*}\left(x\right)=0\right)$$
35	29 34	biimtrid	$$⊢x\subseteq ℝ\to \left(x\preccurlyeq \mathbb{N}\to {vol}^{*}\left(x\right)=0\right)$$
36	35	imdistani	$$⊢\left(x\subseteq ℝ\wedge x\preccurlyeq \mathbb{N}\right)\to \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)$$
37	36	ralimi	$$⊢\forall x\in A\left(x\subseteq ℝ\wedge x\preccurlyeq \mathbb{N}\right)\to \forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)$$
38	21 37	sylbi	$$⊢\left(\bigcup A\subseteq ℝ\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)\to \forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)$$
39	38	ancoms	$$⊢\left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\to \forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)$$
40		foima	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to f\left[\mathbb{N}\right]=A$$
41	40	raleqdv	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \left(\forall x\in f\left[\mathbb{N}\right]\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\leftrightarrow \forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\right)$$
42		fofn	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to fFn\mathbb{N}$$
43		ssid	$$⊢\mathbb{N}\subseteq \mathbb{N}$$
44		sseq1	$$⊢x=f\left(l\right)\to \left(x\subseteq ℝ\leftrightarrow f\left(l\right)\subseteq ℝ\right)$$
45		fveqeq2	$$⊢x=f\left(l\right)\to \left({vol}^{*}\left(x\right)=0\leftrightarrow {vol}^{*}\left(f\left(l\right)\right)=0\right)$$
46	44 45	anbi12d	$$⊢x=f\left(l\right)\to \left(\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\leftrightarrow \left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)$$
47	46	ralima	$$⊢\left(fFn\mathbb{N}\wedge \mathbb{N}\subseteq \mathbb{N}\right)\to \left(\forall x\in f\left[\mathbb{N}\right]\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\leftrightarrow \forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)$$
48	42 43 47	sylancl	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \left(\forall x\in f\left[\mathbb{N}\right]\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\leftrightarrow \forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)$$
49	41 48	bitr3d	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \left(\forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\leftrightarrow \forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)$$
50		fveq2	$$⊢l=n\to f\left(l\right)=f\left(n\right)$$
51	50	sseq1d	$$⊢l=n\to \left(f\left(l\right)\subseteq ℝ\leftrightarrow f\left(n\right)\subseteq ℝ\right)$$
52		2fveq3	$$⊢l=n\to {vol}^{*}\left(f\left(l\right)\right)={vol}^{*}\left(f\left(n\right)\right)$$
53	52	eqeq1d	$$⊢l=n\to \left({vol}^{*}\left(f\left(l\right)\right)=0\leftrightarrow {vol}^{*}\left(f\left(n\right)\right)=0\right)$$
54	51 53	anbi12d	$$⊢l=n\to \left(\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\leftrightarrow \left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)=0\right)\right)$$
55	54	cbvralvw	$$⊢\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\leftrightarrow \forall n\in \mathbb{N}\left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)=0\right)$$
56		0re	$$⊢0\in ℝ$$
57		eleq1a	$$⊢0\in ℝ\to \left({vol}^{*}\left(f\left(n\right)\right)=0\to {vol}^{*}\left(f\left(n\right)\right)\in ℝ\right)$$
58	56 57	ax-mp	$$⊢{vol}^{*}\left(f\left(n\right)\right)=0\to {vol}^{*}\left(f\left(n\right)\right)\in ℝ$$
59	58	anim2i	$$⊢\left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)=0\right)\to \left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)\in ℝ\right)$$
60	59	ralimi	$$⊢\forall n\in \mathbb{N}\left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)=0\right)\to \forall n\in \mathbb{N}\left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)\in ℝ\right)$$
61	55 60	sylbi	$$⊢\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\to \forall n\in \mathbb{N}\left(f\left(n\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(n\right)\right)\in ℝ\right)$$
62	42 61 1	syl2an	$$⊢\left(f:\mathbb{N}\underset{onto}{⟶}A\wedge \forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)\to {vol}^{*}\left(\bigcup _{m\in \mathbb{N}}f\left(m\right)\right)\le sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right),{ℝ}^{*},<\right)$$
63		fofun	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \mathrm{Fun}f$$
64		funiunfv	$$⊢\mathrm{Fun}f\to \bigcup _{m\in \mathbb{N}}f\left(m\right)=\bigcup f\left[\mathbb{N}\right]$$
65	63 64	syl	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \bigcup _{m\in \mathbb{N}}f\left(m\right)=\bigcup f\left[\mathbb{N}\right]$$
66	40	unieqd	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \bigcup f\left[\mathbb{N}\right]=\bigcup A$$
67	65 66	eqtrd	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \bigcup _{m\in \mathbb{N}}f\left(m\right)=\bigcup A$$
68	67	fveq2d	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to {vol}^{*}\left(\bigcup _{m\in \mathbb{N}}f\left(m\right)\right)={vol}^{*}\left(\bigcup A\right)$$
69	68	adantr	$$⊢\left(f:\mathbb{N}\underset{onto}{⟶}A\wedge \forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)\to {vol}^{*}\left(\bigcup _{m\in \mathbb{N}}f\left(m\right)\right)={vol}^{*}\left(\bigcup A\right)$$
70		fveq2	$$⊢l=m\to f\left(l\right)=f\left(m\right)$$
71	70	sseq1d	$$⊢l=m\to \left(f\left(l\right)\subseteq ℝ\leftrightarrow f\left(m\right)\subseteq ℝ\right)$$
72		2fveq3	$$⊢l=m\to {vol}^{*}\left(f\left(l\right)\right)={vol}^{*}\left(f\left(m\right)\right)$$
73	72	eqeq1d	$$⊢l=m\to \left({vol}^{*}\left(f\left(l\right)\right)=0\leftrightarrow {vol}^{*}\left(f\left(m\right)\right)=0\right)$$
74	71 73	anbi12d	$$⊢l=m\to \left(\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\leftrightarrow \left(f\left(m\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(m\right)\right)=0\right)\right)$$
75	74	rspccva	$$⊢\left(\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\wedge m\in \mathbb{N}\right)\to \left(f\left(m\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(m\right)\right)=0\right)$$
76	75	simprd	$$⊢\left(\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\wedge m\in \mathbb{N}\right)\to {vol}^{*}\left(f\left(m\right)\right)=0$$
77	76	mpteq2dva	$$⊢\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\to \left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)=\left(m\in \mathbb{N}⟼0\right)$$
78	77	seqeq3d	$$⊢\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\to seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right)=seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)$$
79	78	rneqd	$$⊢\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\to \mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right)=\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)$$
80	79	supeq1d	$$⊢\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\to sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right),{ℝ}^{*},<\right)$$
81		0cn	$$⊢0\in ℂ$$
82		ser1const	$$⊢\left(0\in ℂ\wedge l\in \mathbb{N}\right)\to seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)=l\cdot 0$$
83	81 82	mpan	$$⊢l\in \mathbb{N}\to seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)=l\cdot 0$$
84		nncn	$$⊢l\in \mathbb{N}\to l\in ℂ$$
85	84	mul01d	$$⊢l\in \mathbb{N}\to l\cdot 0=0$$
86	83 85	eqtrd	$$⊢l\in \mathbb{N}\to seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)=0$$
87	86	mpteq2ia	$$⊢\left(l\in \mathbb{N}⟼seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)\right)=\left(l\in \mathbb{N}⟼0\right)$$
88		fconstmpt	$$⊢\mathbb{N}\times \left\{0\right\}=\left(m\in \mathbb{N}⟼0\right)$$
89		seqeq3	$$⊢\mathbb{N}\times \left\{0\right\}=\left(m\in \mathbb{N}⟼0\right)\to seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)=seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)$$
90	88 89	ax-mp	$$⊢seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)=seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)$$
91		1z	$$⊢1\in \mathbb{Z}$$
92		seqfn	$$⊢1\in \mathbb{Z}\to seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)Fn{\mathbb{Z}}_{\ge 1}$$
93	91 92	ax-mp	$$⊢seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)Fn{\mathbb{Z}}_{\ge 1}$$
94		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
95	94	fneq2i	$$⊢seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)Fn\mathbb{N}\leftrightarrow seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)Fn{\mathbb{Z}}_{\ge 1}$$
96		dffn5	$$⊢seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)Fn\mathbb{N}\leftrightarrow seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)=\left(l\in \mathbb{N}⟼seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)\right)$$
97	95 96	bitr3i	$$⊢seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)Fn{\mathbb{Z}}_{\ge 1}\leftrightarrow seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)=\left(l\in \mathbb{N}⟼seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)\right)$$
98	93 97	mpbi	$$⊢seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)=\left(l\in \mathbb{N}⟼seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)\right)$$
99	90 98	eqtr3i	$$⊢seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)=\left(l\in \mathbb{N}⟼seq1\left(+,\left(\mathbb{N}\times \left\{0\right\}\right)\right)\left(l\right)\right)$$
100		fconstmpt	$$⊢\mathbb{N}\times \left\{0\right\}=\left(l\in \mathbb{N}⟼0\right)$$
101	87 99 100	3eqtr4i	$$⊢seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)=\mathbb{N}\times \left\{0\right\}$$
102	101	rneqi	$$⊢\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)=\mathrm{ran}\left(\mathbb{N}\times \left\{0\right\}\right)$$
103		1nn	$$⊢1\in \mathbb{N}$$
104		ne0i	$$⊢1\in \mathbb{N}\to \mathbb{N}\ne \varnothing$$
105		rnxp	$$⊢\mathbb{N}\ne \varnothing \to \mathrm{ran}\left(\mathbb{N}\times \left\{0\right\}\right)=\left\{0\right\}$$
106	103 104 105	mp2b	$$⊢\mathrm{ran}\left(\mathbb{N}\times \left\{0\right\}\right)=\left\{0\right\}$$
107	102 106	eqtri	$$⊢\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right)=\left\{0\right\}$$
108	107	supeq1i	$$⊢sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right),{ℝ}^{*},<\right)=sup\left(\left\{0\right\},{ℝ}^{*},<\right)$$
109		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
110		0xr	$$⊢0\in {ℝ}^{*}$$
111		supsn	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$$
112	109 110 111	mp2an	$$⊢sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$$
113	108 112	eqtri	$$⊢sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼0\right)\right),{ℝ}^{*},<\right)=0$$
114	80 113	eqtrdi	$$⊢\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\to sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right),{ℝ}^{*},<\right)=0$$
115	114	adantl	$$⊢\left(f:\mathbb{N}\underset{onto}{⟶}A\wedge \forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)\to sup\left(\mathrm{ran}seq1\left(+,\left(m\in \mathbb{N}⟼{vol}^{*}\left(f\left(m\right)\right)\right)\right),{ℝ}^{*},<\right)=0$$
116	62 69 115	3brtr3d	$$⊢\left(f:\mathbb{N}\underset{onto}{⟶}A\wedge \forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\right)\to {vol}^{*}\left(\bigcup A\right)\le 0$$
117	116	ex	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \left(\forall l\in \mathbb{N}\left(f\left(l\right)\subseteq ℝ\wedge {vol}^{*}\left(f\left(l\right)\right)=0\right)\to {vol}^{*}\left(\bigcup A\right)\le 0\right)$$
118	49 117	sylbid	$$⊢f:\mathbb{N}\underset{onto}{⟶}A\to \left(\forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\to {vol}^{*}\left(\bigcup A\right)\le 0\right)$$
119	118	exlimiv	$$⊢\exists ff:\mathbb{N}\underset{onto}{⟶}A\to \left(\forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\to {vol}^{*}\left(\bigcup A\right)\le 0\right)$$
120	119	imp	$$⊢\left(\exists ff:\mathbb{N}\underset{onto}{⟶}A\wedge \forall x\in A\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)=0\right)\right)\to {vol}^{*}\left(\bigcup A\right)\le 0$$
121	17 39 120	syl2an	$$⊢\left(\left(A\ne \varnothing \wedge A\preccurlyeq \mathbb{N}\right)\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to {vol}^{*}\left(\bigcup A\right)\le 0$$
122		ovolcl	$$⊢\bigcup A\subseteq ℝ\to {vol}^{*}\left(\bigcup A\right)\in {ℝ}^{*}$$
123		xrletri3	$$⊢\left(0\in {ℝ}^{*}\wedge {vol}^{*}\left(\bigcup A\right)\in {ℝ}^{*}\right)\to \left(0={vol}^{*}\left(\bigcup A\right)\leftrightarrow \left(0\le {vol}^{*}\left(\bigcup A\right)\wedge {vol}^{*}\left(\bigcup A\right)\le 0\right)\right)$$
124	110 122 123	sylancr	$$⊢\bigcup A\subseteq ℝ\to \left(0={vol}^{*}\left(\bigcup A\right)\leftrightarrow \left(0\le {vol}^{*}\left(\bigcup A\right)\wedge {vol}^{*}\left(\bigcup A\right)\le 0\right)\right)$$
125	124	ad2antll	$$⊢\left(\left(A\ne \varnothing \wedge A\preccurlyeq \mathbb{N}\right)\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to \left(0={vol}^{*}\left(\bigcup A\right)\leftrightarrow \left(0\le {vol}^{*}\left(\bigcup A\right)\wedge {vol}^{*}\left(\bigcup A\right)\le 0\right)\right)$$
126	10 121 125	mpbir2and	$$⊢\left(\left(A\ne \varnothing \wedge A\preccurlyeq \mathbb{N}\right)\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to 0={vol}^{*}\left(\bigcup A\right)$$
127	126	expl	$$⊢A\ne \varnothing \to \left(\left(A\preccurlyeq \mathbb{N}\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to 0={vol}^{*}\left(\bigcup A\right)\right)$$
128	8 127	pm2.61ine	$$⊢\left(A\preccurlyeq \mathbb{N}\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to 0={vol}^{*}\left(\bigcup A\right)$$
129		renepnf	$$⊢0\in ℝ\to 0\ne \mathrm{+\infty }$$
130	56 129	mp1i	$$⊢\bigcup A=ℝ\to 0\ne \mathrm{+\infty }$$
131		fveq2	$$⊢\bigcup A=ℝ\to {vol}^{*}\left(\bigcup A\right)={vol}^{*}\left(ℝ\right)$$
132		ovolre	$$⊢{vol}^{*}\left(ℝ\right)=\mathrm{+\infty }$$
133	131 132	eqtrdi	$$⊢\bigcup A=ℝ\to {vol}^{*}\left(\bigcup A\right)=\mathrm{+\infty }$$
134	130 133	neeqtrrd	$$⊢\bigcup A=ℝ\to 0\ne {vol}^{*}\left(\bigcup A\right)$$
135	134	necon2i	$$⊢0={vol}^{*}\left(\bigcup A\right)\to \bigcup A\ne ℝ$$
136	128 135	syl	$$⊢\left(A\preccurlyeq \mathbb{N}\wedge \left(\forall x\in Ax\preccurlyeq \mathbb{N}\wedge \bigcup A\subseteq ℝ\right)\right)\to \bigcup A\ne ℝ$$
137	136	expr	$$⊢\left(A\preccurlyeq \mathbb{N}\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)\to \left(\bigcup A\subseteq ℝ\to \bigcup A\ne ℝ\right)$$
138		eqimss	$$⊢\bigcup A=ℝ\to \bigcup A\subseteq ℝ$$
139	138	necon3bi	$$⊢\neg \bigcup A\subseteq ℝ\to \bigcup A\ne ℝ$$
140	137 139	pm2.61d1	$$⊢\left(A\preccurlyeq \mathbb{N}\wedge \forall x\in Ax\preccurlyeq \mathbb{N}\right)\to \bigcup A\ne ℝ$$