voliunnfl

Description: voliun is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017)

	Ref	Expression
Hypotheses	voliunnfl.1	$⊢ S = seq 1 (+ G)$
	voliunnfl.2	$⊢ G = (n \in ℕ ⟼ vol (f (n)))$
	voliunnfl.3	$⊢ (\forall n \in ℕ (f (n) \in dom vol \land vol (f (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} f (n)) \to vol (⋃_{n \in ℕ} f (n)) = sup (ran S ℝ^{*} <)$
Assertion	voliunnfl	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$

Proof

Step	Hyp	Ref	Expression
1		voliunnfl.1	$⊢ S = seq 1 (+ G)$
2		voliunnfl.2	$⊢ G = (n \in ℕ ⟼ vol (f (n)))$
3		voliunnfl.3	$⊢ (\forall n \in ℕ (f (n) \in dom vol \land vol (f (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} f (n)) \to vol (⋃_{n \in ℕ} f (n)) = sup (ran S ℝ^{*} <)$
4		unieq	$⊢ A = \emptyset \to ⋃ A = ⋃ \emptyset$
5		uni0	$⊢ ⋃ \emptyset = \emptyset$
6	4 5	eqtrdi	$⊢ A = \emptyset \to ⋃ A = \emptyset$
7	6	fveq2d	$⊢ A = \emptyset \to vol (⋃ A) = vol (\emptyset)$
8		0mbl	$⊢ \emptyset \in dom vol$
9		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
10	8 9	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
11		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
12	10 11	eqtri	$⊢ vol (\emptyset) = 0$
13	7 12	eqtr2di	$⊢ A = \emptyset \to 0 = vol (⋃ A)$
14	13	a1d	$⊢ A = \emptyset \to ((A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = vol (⋃ A))$
15		reldom	$⊢ Rel ≼$
16	15	brrelex1i	$⊢ A ≼ ℕ \to A \in V$
17		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
18	16 17	syl	$⊢ A ≼ ℕ \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
19	18	biimparc	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to \emptyset ≺ A$
20		fodomr	$⊢ (\emptyset ≺ A \land A ≼ ℕ) \to \exists g g : ℕ \underset{onto}{⟶} A$
21	19 20	sylancom	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to \exists g g : ℕ \underset{onto}{⟶} A$
22		unissb	$⊢ ⋃ A \subseteq ℝ \leftrightarrow \forall x \in A x \subseteq ℝ$
23	22	anbi1i	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \leftrightarrow (\forall x \in A x \subseteq ℝ \land \forall x \in A x ≼ ℕ)$
24		r19.26	$⊢ \forall x \in A (x \subseteq ℝ \land x ≼ ℕ) \leftrightarrow (\forall x \in A x \subseteq ℝ \land \forall x \in A x ≼ ℕ)$
25	23 24	bitr4i	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \leftrightarrow \forall x \in A (x \subseteq ℝ \land x ≼ ℕ)$
26		ovolctb2	$⊢ (x \subseteq ℝ \land x ≼ ℕ) \to {vol}^{*} (x) = 0$
27	26	ex	$⊢ x \subseteq ℝ \to (x ≼ ℕ \to {vol}^{*} (x) = 0)$
28	27	imdistani	$⊢ (x \subseteq ℝ \land x ≼ ℕ) \to (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
29	28	ralimi	$⊢ \forall x \in A (x \subseteq ℝ \land x ≼ ℕ) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
30	25 29	sylbi	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
31	30	ancoms	$⊢ (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
32		foima	$⊢ g : ℕ \underset{onto}{⟶} A \to g [ℕ] = A$
33	32	raleqdv	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall x \in g [ℕ] (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall x \in A (x \subseteq ℝ \land {vol}^{} (x) = 0))$
34		fofn	$⊢ g : ℕ \underset{onto}{⟶} A \to g Fn ℕ$
35		ssid	$⊢ ℕ \subseteq ℕ$
36		sseq1	$⊢ x = g (m) \to (x \subseteq ℝ \leftrightarrow g (m) \subseteq ℝ)$
37		fveqeq2	$⊢ x = g (m) \to ({vol}^{} (x) = 0 \leftrightarrow {vol}^{} (g (m)) = 0)$
38	36 37	anbi12d	$⊢ x = g (m) \to ((x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0))$
39	38	ralima	$⊢ (g Fn ℕ \land ℕ \subseteq ℕ) \to (\forall x \in g [ℕ] (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0))$
40	34 35 39	sylancl	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall x \in g [ℕ] (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0))$
41	33 40	bitr3d	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall x \in A (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0))$
42		difss	$⊢ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \subseteq g (m)$
43		ovolssnul	$⊢ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \subseteq g (m) \land g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0) \to {vol}^{} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0$
44	42 43	mp3an1	$⊢ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0) \to {vol}^{} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0$
45		ssdifss	$⊢ g (m) \subseteq ℝ \to g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \subseteq ℝ$
46		nulmbl	$⊢ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \subseteq ℝ \land {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0) \to g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol$
47		mblvol	$⊢ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \to vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l))$
48	47	eqeq1d	$⊢ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \to (vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0 \leftrightarrow {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0)$
49	48	biimpar	$⊢ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0) \to vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0$
50		0re	$⊢ 0 \in ℝ$
51	49 50	eqeltrdi	$⊢ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0) \to vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ$
52	51	expcom	$⊢ {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0 \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \to vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
53	52	ancld	$⊢ {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0 \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ))$
54	53	adantl	$⊢ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \subseteq ℝ \land {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0) \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ))$
55	46 54	mpd	$⊢ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \subseteq ℝ \land {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0) \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
56	45 55	sylan	$⊢ (g (m) \subseteq ℝ \land {vol}^{*} (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = 0) \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
57	44 56	syldan	$⊢ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \to (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
58	57	ralimi	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \to \forall m \in ℕ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
59		fveq2	$⊢ m = n \to g (m) = g (n)$
60		oveq2	$⊢ m = n \to (1 ..^m) = (1 ..^n)$
61	60	iuneq1d	$⊢ m = n \to ⋃_{l \in (1 ..^m)} g (l) = ⋃_{l \in (1 ..^n)} g (l)$
62	59 61	difeq12d	$⊢ m = n \to g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) = g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)$
63		eqid	$⊢ (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l))$
64		fvex	$⊢ g (n) \in V$
65		difexg	$⊢ g (n) \in V \to g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in V$
66	64 65	ax-mp	$⊢ g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in V$
67	62 63 66	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) = g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)$
68	67	eleq1d	$⊢ n \in ℕ \to ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \leftrightarrow g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol)$
69	67	fveq2d	$⊢ n \in ℕ \to vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) = vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))$
70	69	eleq1d	$⊢ n \in ℕ \to (vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ \leftrightarrow vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) \in ℝ)$
71	68 70	anbi12d	$⊢ n \in ℕ \to (((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ) \leftrightarrow (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol \land vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) \in ℝ))$
72	71	ralbiia	$⊢ \forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ) \leftrightarrow \forall n \in ℕ (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol \land vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) \in ℝ)$
73		fveq2	$⊢ n = m \to g (n) = g (m)$
74		oveq2	$⊢ n = m \to (1 ..^n) = (1 ..^m)$
75	74	iuneq1d	$⊢ n = m \to ⋃_{l \in (1 ..^n)} g (l) = ⋃_{l \in (1 ..^m)} g (l)$
76	73 75	difeq12d	$⊢ n = m \to g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) = g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)$
77	76	eleq1d	$⊢ n = m \to (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol \leftrightarrow g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol)$
78	76	fveq2d	$⊢ n = m \to vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l))$
79	78	eleq1d	$⊢ n = m \to (vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) \in ℝ \leftrightarrow vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
80	77 79	anbi12d	$⊢ n = m \to ((g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol \land vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) \in ℝ) \leftrightarrow (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ))$
81	80	cbvralvw	$⊢ \forall n \in ℕ (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol \land vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) \in ℝ) \leftrightarrow \forall m \in ℕ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
82	72 81	bitri	$⊢ \forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ) \leftrightarrow \forall m \in ℕ (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l) \in dom vol \land vol (g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in ℝ)$
83	58 82	sylibr	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \to \forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ)$
84		fveq2	$⊢ n = l \to g (n) = g (l)$
85	84	iundisj2	$⊢ \underset{n \in ℕ}{Disj} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))$
86		disjeq2	$⊢ \forall n \in ℕ (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) = g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \to (\underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \leftrightarrow \underset{n \in ℕ}{Disj} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))$
87	86 67	mprg	$⊢ \underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \leftrightarrow \underset{n \in ℕ}{Disj} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))$
88	85 87	mpbir	$⊢ \underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)$
89		nnex	$⊢ ℕ \in V$
90	89	mptex	$⊢ (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \in V$
91		fveq1	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to f (n) = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)$
92	91	eleq1d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to (f (n) \in dom vol \leftrightarrow (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol)$
93	91	fveq2d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to vol (f (n)) = vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n))$
94	93	eleq1d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to (vol (f (n)) \in ℝ \leftrightarrow vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ)$
95	92 94	anbi12d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to ((f (n) \in dom vol \land vol (f (n)) \in ℝ) \leftrightarrow ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ))$
96	95	ralbidv	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to (\forall n \in ℕ (f (n) \in dom vol \land vol (f (n)) \in ℝ) \leftrightarrow \forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ))$
97	91	adantr	$⊢ (f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \land n \in ℕ) \to f (n) = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)$
98	97	disjeq2dv	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to (\underset{n \in ℕ}{Disj} f (n) \leftrightarrow \underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n))$
99	96 98	anbi12d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to ((\forall n \in ℕ (f (n) \in dom vol \land vol (f (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} f (n)) \leftrightarrow (\forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))$
100	91	iuneq2d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to ⋃_{n \in ℕ} f (n) = ⋃_{n \in ℕ} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)$
101	100	fveq2d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to vol (⋃_{n \in ℕ} f (n)) = vol (⋃_{n \in ℕ} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n))$
102		seqeq3	$⊢ G = (n \in ℕ ⟼ vol (f (n))) \to seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ vol (f (n))))$
103	2 102	ax-mp	$⊢ seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ vol (f (n))))$
104	1 103	eqtri	$⊢ S = seq 1 (+ (n \in ℕ ⟼ vol (f (n))))$
105	104	rneqi	$⊢ ran S = ran seq 1 (+ (n \in ℕ ⟼ vol (f (n))))$
106	105	supeq1i	$⊢ sup (ran S ℝ^{} <) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (f (n)))) ℝ^{} <)$
107	93	mpteq2dv	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to (n \in ℕ ⟼ vol (f (n))) = (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))$
108	107	seqeq3d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to seq 1 (+ (n \in ℕ ⟼ vol (f (n)))) = seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n))))$
109	108	rneqd	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to ran seq 1 (+ (n \in ℕ ⟼ vol (f (n)))) = ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n))))$
110	109	supeq1d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to sup (ran seq 1 (+ (n \in ℕ ⟼ vol (f (n)))) ℝ^{} <) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) ℝ^{} <)$
111	106 110	eqtrid	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to sup (ran S ℝ^{} <) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) ℝ^{} <)$
112	101 111	eqeq12d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to (vol (⋃_{n \in ℕ} f (n)) = sup (ran S ℝ^{} <) \leftrightarrow vol (⋃_{n \in ℕ} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) ℝ^{} <))$
113	99 112	imbi12d	$⊢ f = (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) \to (((\forall n \in ℕ (f (n) \in dom vol \land vol (f (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} f (n)) \to vol (⋃_{n \in ℕ} f (n)) = sup (ran S ℝ^{} <)) \leftrightarrow ((\forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \to vol (⋃_{n \in ℕ} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) ℝ^{} <)))$
114	90 113 3	vtocl	$⊢ (\forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \to vol (⋃_{n \in ℕ} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) ℝ^{*} <)$
115	67	iuneq2i	$⊢ ⋃_{n \in ℕ} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) = ⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))$
116	115	fveq2i	$⊢ vol (⋃_{n \in ℕ} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) = vol (⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))$
117	69	mpteq2ia	$⊢ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n))) = (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))$
118		seqeq3	$⊢ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n))) = (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))) \to seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) = seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))))$
119	117 118	ax-mp	$⊢ seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) = seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))))$
120	119	rneqi	$⊢ ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) = ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))))$
121	120	supeq1i	$⊢ sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)))) ℝ^{} <) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) ℝ^{} <)$
122	114 116 121	3eqtr3g	$⊢ (\forall n \in ℕ ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n) \in dom vol \land vol ((m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} (m \in ℕ ⟼ g (m) ∖ ⋃_{l \in (1 ..^m)} g (l)) (n)) \to vol (⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) ℝ^{*} <)$
123	83 88 122	sylancl	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0) \to vol (⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) ℝ^{} <)$
124	123	adantl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0)) \to vol (⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) ℝ^{} <)$
125	84	iundisj	$⊢ ⋃_{n \in ℕ} g (n) = ⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))$
126		fofun	$⊢ g : ℕ \underset{onto}{⟶} A \to Fun g$
127		funiunfv	$⊢ Fun g \to ⋃_{n \in ℕ} g (n) = ⋃ g [ℕ]$
128	126 127	syl	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃_{n \in ℕ} g (n) = ⋃ g [ℕ]$
129	125 128	eqtr3id	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = ⋃ g [ℕ]$
130	32	unieqd	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃ g [ℕ] = ⋃ A$
131	129 130	eqtrd	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = ⋃ A$
132	131	fveq2d	$⊢ g : ℕ \underset{onto}{⟶} A \to vol (⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))) = vol (⋃ A)$
133	132	adantr	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0)) \to vol (⋃_{n \in ℕ} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))) = vol (⋃ A)$
134	59	sseq1d	$⊢ m = n \to (g (m) \subseteq ℝ \leftrightarrow g (n) \subseteq ℝ)$
135	59	fveqeq2d	$⊢ m = n \to ({vol}^{} (g (m)) = 0 \leftrightarrow {vol}^{} (g (n)) = 0)$
136	134 135	anbi12d	$⊢ m = n \to ((g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0) \leftrightarrow (g (n) \subseteq ℝ \land {vol}^{} (g (n)) = 0))$
137	136	rspccva	$⊢ (\forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0) \land n \in ℕ) \to (g (n) \subseteq ℝ \land {vol}^{} (g (n)) = 0)$
138		ssdifss	$⊢ g (n) \subseteq ℝ \to g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \subseteq ℝ$
139	138	adantr	$⊢ (g (n) \subseteq ℝ \land {vol}^{*} (g (n)) = 0) \to g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \subseteq ℝ$
140		difss	$⊢ g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \subseteq g (n)$
141		ovolssnul	$⊢ (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \subseteq g (n) \land g (n) \subseteq ℝ \land {vol}^{} (g (n)) = 0) \to {vol}^{} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = 0$
142	140 141	mp3an1	$⊢ (g (n) \subseteq ℝ \land {vol}^{} (g (n)) = 0) \to {vol}^{} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = 0$
143	139 142	jca	$⊢ (g (n) \subseteq ℝ \land {vol}^{} (g (n)) = 0) \to (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \subseteq ℝ \land {vol}^{} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = 0)$
144		nulmbl	$⊢ (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \subseteq ℝ \land {vol}^{*} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = 0) \to g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol$
145		mblvol	$⊢ g (n) ∖ ⋃_{l \in (1 ..^n)} g (l) \in dom vol \to vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = {vol}^{*} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))$
146	143 144 145	3syl	$⊢ (g (n) \subseteq ℝ \land {vol}^{} (g (n)) = 0) \to vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = {vol}^{} (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))$
147	146 142	eqtrd	$⊢ (g (n) \subseteq ℝ \land {vol}^{*} (g (n)) = 0) \to vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = 0$
148	137 147	syl	$⊢ (\forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \land n \in ℕ) \to vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)) = 0$
149	148	mpteq2dva	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \to (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l))) = (n \in ℕ ⟼ 0)$
150	149	seqeq3d	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \to seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) = seq 1 (+ (n \in ℕ ⟼ 0))$
151	150	rneqd	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \to ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) = ran seq 1 (+ (n \in ℕ ⟼ 0))$
152	151	supeq1d	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0) \to sup (ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) ℝ^{} <) = sup (ran seq 1 (+ (n \in ℕ ⟼ 0)) ℝ^{*} <)$
153		0cn	$⊢ 0 \in ℂ$
154		ser1const	$⊢ (0 \in ℂ \land m \in ℕ) \to seq 1 (+ (ℕ \times \{0\})) (m) = m \cdot 0$
155	153 154	mpan	$⊢ m \in ℕ \to seq 1 (+ (ℕ \times \{0\})) (m) = m \cdot 0$
156		nncn	$⊢ m \in ℕ \to m \in ℂ$
157	156	mul01d	$⊢ m \in ℕ \to m \cdot 0 = 0$
158	155 157	eqtrd	$⊢ m \in ℕ \to seq 1 (+ (ℕ \times \{0\})) (m) = 0$
159	158	mpteq2ia	$⊢ (m \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (m)) = (m \in ℕ ⟼ 0)$
160		fconstmpt	$⊢ ℕ \times \{0\} = (n \in ℕ ⟼ 0)$
161		seqeq3	$⊢ ℕ \times \{0\} = (n \in ℕ ⟼ 0) \to seq 1 (+ (ℕ \times \{0\})) = seq 1 (+ (n \in ℕ ⟼ 0))$
162	160 161	ax-mp	$⊢ seq 1 (+ (ℕ \times \{0\})) = seq 1 (+ (n \in ℕ ⟼ 0))$
163		1z	$⊢ 1 \in ℤ$
164		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1}$
165	163 164	ax-mp	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1}$
166		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
167	166	fneq2i	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℕ \leftrightarrow seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1}$
168		dffn5	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℕ \leftrightarrow seq 1 (+ (ℕ \times \{0\})) = (m \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (m))$
169	167 168	bitr3i	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1} \leftrightarrow seq 1 (+ (ℕ \times \{0\})) = (m \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (m))$
170	165 169	mpbi	$⊢ seq 1 (+ (ℕ \times \{0\})) = (m \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (m))$
171	162 170	eqtr3i	$⊢ seq 1 (+ (n \in ℕ ⟼ 0)) = (m \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (m))$
172		fconstmpt	$⊢ ℕ \times \{0\} = (m \in ℕ ⟼ 0)$
173	159 171 172	3eqtr4i	$⊢ seq 1 (+ (n \in ℕ ⟼ 0)) = ℕ \times \{0\}$
174	173	rneqi	$⊢ ran seq 1 (+ (n \in ℕ ⟼ 0)) = ran (ℕ \times \{0\})$
175		1nn	$⊢ 1 \in ℕ$
176		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
177		rnxp	$⊢ ℕ \neq \emptyset \to ran (ℕ \times \{0\}) = \{0\}$
178	175 176 177	mp2b	$⊢ ran (ℕ \times \{0\}) = \{0\}$
179	174 178	eqtri	$⊢ ran seq 1 (+ (n \in ℕ ⟼ 0)) = \{0\}$
180	179	supeq1i	$⊢ sup (ran seq 1 (+ (n \in ℕ ⟼ 0)) ℝ^{} <) = sup (\{0\} ℝ^{} <)$
181		xrltso	$⊢ < Or ℝ^{*}$
182		0xr	$⊢ 0 \in ℝ^{*}$
183		supsn	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{}) \to sup (\{0\} ℝ^{*} <) = 0$
184	181 182 183	mp2an	$⊢ sup (\{0\} ℝ^{*} <) = 0$
185	180 184	eqtri	$⊢ sup (ran seq 1 (+ (n \in ℕ ⟼ 0)) ℝ^{*} <) = 0$
186	152 185	eqtrdi	$⊢ \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0) \to sup (ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) ℝ^{} <) = 0$
187	186	adantl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{} (g (m)) = 0)) \to sup (ran seq 1 (+ (n \in ℕ ⟼ vol (g (n) ∖ ⋃_{l \in (1 ..^n)} g (l)))) ℝ^{} <) = 0$
188	124 133 187	3eqtr3rd	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0)) \to 0 = vol (⋃ A)$
189	188	ex	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall m \in ℕ (g (m) \subseteq ℝ \land {vol}^{*} (g (m)) = 0) \to 0 = vol (⋃ A))$
190	41 189	sylbid	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) = 0) \to 0 = vol (⋃ A))$
191	31 190	syl5	$⊢ g : ℕ \underset{onto}{⟶} A \to ((\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to 0 = vol (⋃ A))$
192	191	exlimiv	$⊢ \exists g g : ℕ \underset{onto}{⟶} A \to ((\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to 0 = vol (⋃ A))$
193	21 192	syl	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to ((\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to 0 = vol (⋃ A))$
194	193	expimpd	$⊢ A \neq \emptyset \to ((A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = vol (⋃ A))$
195	14 194	pm2.61ine	$⊢ (A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = vol (⋃ A)$
196		renepnf	$⊢ 0 \in ℝ \to 0 \neq +∞$
197	50 196	mp1i	$⊢ ⋃ A = ℝ \to 0 \neq +∞$
198		fveq2	$⊢ ⋃ A = ℝ \to vol (⋃ A) = vol (ℝ)$
199		rembl	$⊢ ℝ \in dom vol$
200		mblvol	$⊢ ℝ \in dom vol \to vol (ℝ) = {vol}^{*} (ℝ)$
201	199 200	ax-mp	$⊢ vol (ℝ) = {vol}^{*} (ℝ)$
202		ovolre	$⊢ {vol}^{*} (ℝ) = +∞$
203	201 202	eqtri	$⊢ vol (ℝ) = +∞$
204	198 203	eqtrdi	$⊢ ⋃ A = ℝ \to vol (⋃ A) = +∞$
205	197 204	neeqtrrd	$⊢ ⋃ A = ℝ \to 0 \neq vol (⋃ A)$
206	205	necon2i	$⊢ 0 = vol (⋃ A) \to ⋃ A \neq ℝ$
207	195 206	syl	$⊢ (A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to ⋃ A \neq ℝ$
208	207	expr	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to (⋃ A \subseteq ℝ \to ⋃ A \neq ℝ)$
209		eqimss	$⊢ ⋃ A = ℝ \to ⋃ A \subseteq ℝ$
210	209	necon3bi	$⊢ \neg ⋃ A \subseteq ℝ \to ⋃ A \neq ℝ$
211	208 210	pm2.61d1	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$

Metamath Proof Explorer

Theorem voliunnfl

Proof