volsupnfl

Description: volsup is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018)

		Ref	Expression
	Hypothesis	volsupnfl.0	$⊢ (f : ℕ ⟶ dom vol \land \forall n \in ℕ f (n) \subseteq f (n + 1)) \to vol (⋃ ran f) = sup (vol [ran f] ℝ^{*} <)$
	Assertion	volsupnfl	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$

Proof

Step	Hyp	Ref	Expression
1		volsupnfl.0	$⊢ (f : ℕ ⟶ dom vol \land \forall n \in ℕ f (n) \subseteq f (n + 1)) \to vol (⋃ ran f) = sup (vol [ran f] ℝ^{*} <)$
2		unieq	$⊢ A = \emptyset \to ⋃ A = ⋃ \emptyset$
3		uni0	$⊢ ⋃ \emptyset = \emptyset$
4	2 3	eqtrdi	$⊢ A = \emptyset \to ⋃ A = \emptyset$
5	4	fveq2d	$⊢ A = \emptyset \to vol (⋃ A) = vol (\emptyset)$
6		0mbl	$⊢ \emptyset \in dom vol$
7		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
8	6 7	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
9		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
10	8 9	eqtri	$⊢ vol (\emptyset) = 0$
11	5 10	eqtr2di	$⊢ A = \emptyset \to 0 = vol (⋃ A)$
12	11	a1d	$⊢ A = \emptyset \to ((A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = vol (⋃ A))$
13		reldom	$⊢ Rel ≼$
14	13	brrelex1i	$⊢ A ≼ ℕ \to A \in V$
15		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
16	14 15	syl	$⊢ A ≼ ℕ \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
17	16	biimparc	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to \emptyset ≺ A$
18		fodomr	$⊢ (\emptyset ≺ A \land A ≼ ℕ) \to \exists g g : ℕ \underset{onto}{⟶} A$
19	17 18	sylancom	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to \exists g g : ℕ \underset{onto}{⟶} A$
20		unissb	$⊢ ⋃ A \subseteq ℝ \leftrightarrow \forall x \in A x \subseteq ℝ$
21	20	anbi1i	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \leftrightarrow (\forall x \in A x \subseteq ℝ \land \forall x \in A x ≼ ℕ)$
22		r19.26	$⊢ \forall x \in A (x \subseteq ℝ \land x ≼ ℕ) \leftrightarrow (\forall x \in A x \subseteq ℝ \land \forall x \in A x ≼ ℕ)$
23	21 22	bitr4i	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \leftrightarrow \forall x \in A (x \subseteq ℝ \land x ≼ ℕ)$
24		ovolctb2	$⊢ (x \subseteq ℝ \land x ≼ ℕ) \to {vol}^{*} (x) = 0$
25		nulmbl	$⊢ (x \subseteq ℝ \land {vol}^{*} (x) = 0) \to x \in dom vol$
26		mblvol	$⊢ x \in dom vol \to vol (x) = {vol}^{*} (x)$
27		eqtr	$⊢ (vol (x) = {vol}^{} (x) \land {vol}^{} (x) = 0) \to vol (x) = 0$
28	27	expcom	$⊢ {vol}^{} (x) = 0 \to (vol (x) = {vol}^{} (x) \to vol (x) = 0)$
29	26 28	syl5	$⊢ {vol}^{*} (x) = 0 \to (x \in dom vol \to vol (x) = 0)$
30	29	adantl	$⊢ (x \subseteq ℝ \land {vol}^{*} (x) = 0) \to (x \in dom vol \to vol (x) = 0)$
31	25 30	jcai	$⊢ (x \subseteq ℝ \land {vol}^{*} (x) = 0) \to (x \in dom vol \land vol (x) = 0)$
32	24 31	syldan	$⊢ (x \subseteq ℝ \land x ≼ ℕ) \to (x \in dom vol \land vol (x) = 0)$
33	32	ralimi	$⊢ \forall x \in A (x \subseteq ℝ \land x ≼ ℕ) \to \forall x \in A (x \in dom vol \land vol (x) = 0)$
34	23 33	sylbi	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \to \forall x \in A (x \in dom vol \land vol (x) = 0)$
35	34	ancoms	$⊢ (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to \forall x \in A (x \in dom vol \land vol (x) = 0)$
36		fzfi	$⊢ (1 \dots m) \in Fin$
37		fzssuz	$⊢ (1 \dots m) \subseteq ℤ_{\geq 1}$
38		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
39	37 38	sseqtrri	$⊢ (1 \dots m) \subseteq ℕ$
40		fof	$⊢ g : ℕ \underset{onto}{⟶} A \to g : ℕ ⟶ A$
41	40	ffvelcdmda	$⊢ (g : ℕ \underset{onto}{⟶} A \land l \in ℕ) \to g (l) \in A$
42		eleq1	$⊢ x = g (l) \to (x \in dom vol \leftrightarrow g (l) \in dom vol)$
43		fveqeq2	$⊢ x = g (l) \to (vol (x) = 0 \leftrightarrow vol (g (l)) = 0)$
44	42 43	anbi12d	$⊢ x = g (l) \to ((x \in dom vol \land vol (x) = 0) \leftrightarrow (g (l) \in dom vol \land vol (g (l)) = 0))$
45	44	rspccva	$⊢ (\forall x \in A (x \in dom vol \land vol (x) = 0) \land g (l) \in A) \to (g (l) \in dom vol \land vol (g (l)) = 0)$
46	45	simpld	$⊢ (\forall x \in A (x \in dom vol \land vol (x) = 0) \land g (l) \in A) \to g (l) \in dom vol$
47	46	ancoms	$⊢ (g (l) \in A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to g (l) \in dom vol$
48	41 47	sylan	$⊢ ((g : ℕ \underset{onto}{⟶} A \land l \in ℕ) \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to g (l) \in dom vol$
49	48	an32s	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land l \in ℕ) \to g (l) \in dom vol$
50	49	ralrimiva	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall l \in ℕ g (l) \in dom vol$
51		ssralv	$⊢ (1 \dots m) \subseteq ℕ \to (\forall l \in ℕ g (l) \in dom vol \to \forall l \in (1 \dots m) g (l) \in dom vol)$
52	39 50 51	mpsyl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall l \in (1 \dots m) g (l) \in dom vol$
53		finiunmbl	$⊢ ((1 \dots m) \in Fin \land \forall l \in (1 \dots m) g (l) \in dom vol) \to ⋃_{l = 1}^{m} g (l) \in dom vol$
54	36 52 53	sylancr	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to ⋃_{l = 1}^{m} g (l) \in dom vol$
55	54	adantr	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to ⋃_{l = 1}^{m} g (l) \in dom vol$
56	55	fmpttd	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) : ℕ ⟶ dom vol$
57		fzssp1	$⊢ (1 \dots n) \subseteq (1 \dots n + 1)$
58		iunss1	$⊢ (1 \dots n) \subseteq (1 \dots n + 1) \to ⋃_{l = 1}^{n} g (l) \subseteq ⋃_{l = 1}^{n + 1} g (l)$
59	57 58	ax-mp	$⊢ ⋃_{l = 1}^{n} g (l) \subseteq ⋃_{l = 1}^{n + 1} g (l)$
60		oveq2	$⊢ m = n \to (1 \dots m) = (1 \dots n)$
61	60	iuneq1d	$⊢ m = n \to ⋃_{l = 1}^{m} g (l) = ⋃_{l = 1}^{n} g (l)$
62		eqid	$⊢ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))$
63		ovex	$⊢ (1 \dots n) \in V$
64		fvex	$⊢ g (l) \in V$
65	63 64	iunex	$⊢ ⋃_{l = 1}^{n} g (l) \in V$
66	61 62 65	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) = ⋃_{l = 1}^{n} g (l)$
67		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
68		oveq2	$⊢ m = n + 1 \to (1 \dots m) = (1 \dots n + 1)$
69	68	iuneq1d	$⊢ m = n + 1 \to ⋃_{l = 1}^{m} g (l) = ⋃_{l = 1}^{n + 1} g (l)$
70		ovex	$⊢ (1 \dots n + 1) \in V$
71	70 64	iunex	$⊢ ⋃_{l = 1}^{n + 1} g (l) \in V$
72	69 62 71	fvmpt	$⊢ n + 1 \in ℕ \to (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1) = ⋃_{l = 1}^{n + 1} g (l)$
73	67 72	syl	$⊢ n \in ℕ \to (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1) = ⋃_{l = 1}^{n + 1} g (l)$
74	66 73	sseq12d	$⊢ n \in ℕ \to ((m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1) \leftrightarrow ⋃_{l = 1}^{n} g (l) \subseteq ⋃_{l = 1}^{n + 1} g (l))$
75	59 74	mpbiri	$⊢ n \in ℕ \to (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1)$
76	75	rgen	$⊢ \forall n \in ℕ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1)$
77		nnex	$⊢ ℕ \in V$
78	77	mptex	$⊢ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \in V$
79		feq1	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to (f : ℕ ⟶ dom vol \leftrightarrow (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) : ℕ ⟶ dom vol)$
80		fveq1	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to f (n) = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n)$
81		fveq1	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to f (n + 1) = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1)$
82	80 81	sseq12d	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to (f (n) \subseteq f (n + 1) \leftrightarrow (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1))$
83	82	ralbidv	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to (\forall n \in ℕ f (n) \subseteq f (n + 1) \leftrightarrow \forall n \in ℕ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1))$
84	79 83	anbi12d	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to ((f : ℕ ⟶ dom vol \land \forall n \in ℕ f (n) \subseteq f (n + 1)) \leftrightarrow ((m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) : ℕ ⟶ dom vol \land \forall n \in ℕ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1)))$
85		rneq	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to ran f = ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))$
86	85	unieqd	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to ⋃ ran f = ⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))$
87	86	fveq2d	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to vol (⋃ ran f) = vol (⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)))$
88	85	imaeq2d	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to vol [ran f] = vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))]$
89	88	supeq1d	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to sup (vol [ran f] ℝ^{} <) = sup (vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] ℝ^{} <)$
90	87 89	eqeq12d	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to (vol (⋃ ran f) = sup (vol [ran f] ℝ^{} <) \leftrightarrow vol (⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = sup (vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] ℝ^{} <))$
91	84 90	imbi12d	$⊢ f = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \to (((f : ℕ ⟶ dom vol \land \forall n \in ℕ f (n) \subseteq f (n + 1)) \to vol (⋃ ran f) = sup (vol [ran f] ℝ^{} <)) \leftrightarrow (((m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) : ℕ ⟶ dom vol \land \forall n \in ℕ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1)) \to vol (⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = sup (vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] ℝ^{} <)))$
92	78 91 1	vtocl	$⊢ ((m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) : ℕ ⟶ dom vol \land \forall n \in ℕ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n) \subseteq (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) (n + 1)) \to vol (⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = sup (vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] ℝ^{*} <)$
93	56 76 92	sylancl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol (⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = sup (vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] ℝ^{*} <)$
94		df-iun	$⊢ ⋃_{x \in ℕ} g (x) = \{n \| \exists x \in ℕ n \in g (x)\}$
95		eluzfz2	$⊢ x \in ℤ_{\geq 1} \to x \in (1 \dots x)$
96	95 38	eleq2s	$⊢ x \in ℕ \to x \in (1 \dots x)$
97		fveq2	$⊢ l = x \to g (l) = g (x)$
98	97	eleq2d	$⊢ l = x \to (n \in g (l) \leftrightarrow n \in g (x))$
99	98	rspcev	$⊢ (x \in (1 \dots x) \land n \in g (x)) \to \exists l \in (1 \dots x) n \in g (l)$
100	96 99	sylan	$⊢ (x \in ℕ \land n \in g (x)) \to \exists l \in (1 \dots x) n \in g (l)$
101		oveq2	$⊢ m = x \to (1 \dots m) = (1 \dots x)$
102	101	rexeqdv	$⊢ m = x \to (\exists l \in (1 \dots m) n \in g (l) \leftrightarrow \exists l \in (1 \dots x) n \in g (l))$
103	102	rspcev	$⊢ (x \in ℕ \land \exists l \in (1 \dots x) n \in g (l)) \to \exists m \in ℕ \exists l \in (1 \dots m) n \in g (l)$
104	100 103	syldan	$⊢ (x \in ℕ \land n \in g (x)) \to \exists m \in ℕ \exists l \in (1 \dots m) n \in g (l)$
105	104	rexlimiva	$⊢ \exists x \in ℕ n \in g (x) \to \exists m \in ℕ \exists l \in (1 \dots m) n \in g (l)$
106		ssrexv	$⊢ (1 \dots m) \subseteq ℕ \to (\exists l \in (1 \dots m) n \in g (l) \to \exists l \in ℕ n \in g (l))$
107	39 106	ax-mp	$⊢ \exists l \in (1 \dots m) n \in g (l) \to \exists l \in ℕ n \in g (l)$
108	98	cbvrexvw	$⊢ \exists l \in ℕ n \in g (l) \leftrightarrow \exists x \in ℕ n \in g (x)$
109	107 108	sylib	$⊢ \exists l \in (1 \dots m) n \in g (l) \to \exists x \in ℕ n \in g (x)$
110	109	rexlimivw	$⊢ \exists m \in ℕ \exists l \in (1 \dots m) n \in g (l) \to \exists x \in ℕ n \in g (x)$
111	105 110	impbii	$⊢ \exists x \in ℕ n \in g (x) \leftrightarrow \exists m \in ℕ \exists l \in (1 \dots m) n \in g (l)$
112		eliun	$⊢ n \in ⋃_{l = 1}^{m} g (l) \leftrightarrow \exists l \in (1 \dots m) n \in g (l)$
113	112	rexbii	$⊢ \exists m \in ℕ n \in ⋃_{l = 1}^{m} g (l) \leftrightarrow \exists m \in ℕ \exists l \in (1 \dots m) n \in g (l)$
114	111 113	bitr4i	$⊢ \exists x \in ℕ n \in g (x) \leftrightarrow \exists m \in ℕ n \in ⋃_{l = 1}^{m} g (l)$
115	114	abbii	$⊢ \{n \| \exists x \in ℕ n \in g (x)\} = \{n \| \exists m \in ℕ n \in ⋃_{l = 1}^{m} g (l)\}$
116	94 115	eqtri	$⊢ ⋃_{x \in ℕ} g (x) = \{n \| \exists m \in ℕ n \in ⋃_{l = 1}^{m} g (l)\}$
117		df-iun	$⊢ ⋃_{m \in ℕ} ⋃_{l = 1}^{m} g (l) = \{n \| \exists m \in ℕ n \in ⋃_{l = 1}^{m} g (l)\}$
118		ovex	$⊢ (1 \dots m) \in V$
119	118 64	iunex	$⊢ ⋃_{l = 1}^{m} g (l) \in V$
120	119	dfiun3	$⊢ ⋃_{m \in ℕ} ⋃_{l = 1}^{m} g (l) = ⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))$
121	116 117 120	3eqtr2i	$⊢ ⋃_{x \in ℕ} g (x) = ⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))$
122		fofn	$⊢ g : ℕ \underset{onto}{⟶} A \to g Fn ℕ$
123		fniunfv	$⊢ g Fn ℕ \to ⋃_{x \in ℕ} g (x) = ⋃ ran g$
124	122 123	syl	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃_{x \in ℕ} g (x) = ⋃ ran g$
125		forn	$⊢ g : ℕ \underset{onto}{⟶} A \to ran g = A$
126	125	unieqd	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃ ran g = ⋃ A$
127	124 126	eqtrd	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃_{x \in ℕ} g (x) = ⋃ A$
128	121 127	eqtr3id	$⊢ g : ℕ \underset{onto}{⟶} A \to ⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) = ⋃ A$
129	128	fveq2d	$⊢ g : ℕ \underset{onto}{⟶} A \to vol (⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = vol (⋃ A)$
130	129	adantr	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol (⋃ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = vol (⋃ A)$
131		rnco2	$⊢ ran (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))]$
132		eqidd	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) = (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))$
133		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
134	133	a1i	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol : dom vol ⟶ [0, +∞]$
135	134	feqmptd	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol = (n \in dom vol ⟼ vol (n))$
136		fveq2	$⊢ n = ⋃_{l = 1}^{m} g (l) \to vol (n) = vol (⋃_{l = 1}^{m} g (l))$
137	55 132 135 136	fmptco	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) = (m \in ℕ ⟼ vol (⋃_{l = 1}^{m} g (l)))$
138		mblvol	$⊢ ⋃_{l = 1}^{m} g (l) \in dom vol \to vol (⋃_{l = 1}^{m} g (l)) = {vol}^{*} (⋃_{l = 1}^{m} g (l))$
139	55 138	syl	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to vol (⋃_{l = 1}^{m} g (l)) = {vol}^{*} (⋃_{l = 1}^{m} g (l))$
140		mblss	$⊢ x \in dom vol \to x \subseteq ℝ$
141	140	adantr	$⊢ (x \in dom vol \land vol (x) = 0) \to x \subseteq ℝ$
142	26	eqeq1d	$⊢ x \in dom vol \to (vol (x) = 0 \leftrightarrow {vol}^{*} (x) = 0)$
143		0re	$⊢ 0 \in ℝ$
144		eleq1a	$⊢ 0 \in ℝ \to ({vol}^{} (x) = 0 \to {vol}^{} (x) \in ℝ)$
145	143 144	ax-mp	$⊢ {vol}^{} (x) = 0 \to {vol}^{} (x) \in ℝ$
146	142 145	biimtrdi	$⊢ x \in dom vol \to (vol (x) = 0 \to {vol}^{*} (x) \in ℝ)$
147	146	imp	$⊢ (x \in dom vol \land vol (x) = 0) \to {vol}^{*} (x) \in ℝ$
148	141 147	jca	$⊢ (x \in dom vol \land vol (x) = 0) \to (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)$
149	148	ralimi	$⊢ \forall x \in A (x \in dom vol \land vol (x) = 0) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)$
150	149	adantl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)$
151		ssid	$⊢ ℕ \subseteq ℕ$
152		sseq1	$⊢ x = g (l) \to (x \subseteq ℝ \leftrightarrow g (l) \subseteq ℝ)$
153		fveq2	$⊢ x = g (l) \to {vol}^{} (x) = {vol}^{} (g (l))$
154	153	eleq1d	$⊢ x = g (l) \to ({vol}^{} (x) \in ℝ \leftrightarrow {vol}^{} (g (l)) \in ℝ)$
155	152 154	anbi12d	$⊢ x = g (l) \to ((x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \leftrightarrow (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ))$
156	155	ralima	$⊢ (g Fn ℕ \land ℕ \subseteq ℕ) \to (\forall x \in g [ℕ] (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \leftrightarrow \forall l \in ℕ (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ))$
157	122 151 156	sylancl	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall x \in g [ℕ] (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \leftrightarrow \forall l \in ℕ (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ))$
158		foima	$⊢ g : ℕ \underset{onto}{⟶} A \to g [ℕ] = A$
159	158	raleqdv	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall x \in g [ℕ] (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \leftrightarrow \forall x \in A (x \subseteq ℝ \land {vol}^{} (x) \in ℝ))$
160	157 159	bitr3d	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall l \in ℕ (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ) \leftrightarrow \forall x \in A (x \subseteq ℝ \land {vol}^{} (x) \in ℝ))$
161	160	adantr	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to (\forall l \in ℕ (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ) \leftrightarrow \forall x \in A (x \subseteq ℝ \land {vol}^{} (x) \in ℝ))$
162	150 161	mpbird	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall l \in ℕ (g (l) \subseteq ℝ \land {vol}^{*} (g (l)) \in ℝ)$
163		ssralv	$⊢ (1 \dots m) \subseteq ℕ \to (\forall l \in ℕ (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ) \to \forall l \in (1 \dots m) (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ))$
164	39 162 163	mpsyl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall l \in (1 \dots m) (g (l) \subseteq ℝ \land {vol}^{*} (g (l)) \in ℝ)$
165	164	adantr	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to \forall l \in (1 \dots m) (g (l) \subseteq ℝ \land {vol}^{*} (g (l)) \in ℝ)$
166		ovolfiniun	$⊢ ((1 \dots m) \in Fin \land \forall l \in (1 \dots m) (g (l) \subseteq ℝ \land {vol}^{} (g (l)) \in ℝ)) \to {vol}^{} (⋃_{l = 1}^{m} g (l)) \leq \sum_{l = 1}^{m} {vol}^{*} (g (l))$
167	36 165 166	sylancr	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to {vol}^{} (⋃_{l = 1}^{m} g (l)) \leq \sum_{l = 1}^{m} {vol}^{} (g (l))$
168		mblvol	$⊢ g (l) \in dom vol \to vol (g (l)) = {vol}^{*} (g (l))$
169	49 168	syl	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land l \in ℕ) \to vol (g (l)) = {vol}^{*} (g (l))$
170	45	simprd	$⊢ (\forall x \in A (x \in dom vol \land vol (x) = 0) \land g (l) \in A) \to vol (g (l)) = 0$
171	41 170	sylan2	$⊢ (\forall x \in A (x \in dom vol \land vol (x) = 0) \land (g : ℕ \underset{onto}{⟶} A \land l \in ℕ)) \to vol (g (l)) = 0$
172	171	ancoms	$⊢ ((g : ℕ \underset{onto}{⟶} A \land l \in ℕ) \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol (g (l)) = 0$
173	172	an32s	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land l \in ℕ) \to vol (g (l)) = 0$
174	169 173	eqtr3d	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land l \in ℕ) \to {vol}^{*} (g (l)) = 0$
175	174	ralrimiva	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall l \in ℕ {vol}^{*} (g (l)) = 0$
176		ssralv	$⊢ (1 \dots m) \subseteq ℕ \to (\forall l \in ℕ {vol}^{} (g (l)) = 0 \to \forall l \in (1 \dots m) {vol}^{} (g (l)) = 0)$
177	39 175 176	mpsyl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall l \in (1 \dots m) {vol}^{*} (g (l)) = 0$
178	177	adantr	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to \forall l \in (1 \dots m) {vol}^{*} (g (l)) = 0$
179	178	sumeq2d	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to \sum_{l = 1}^{m} {vol}^{*} (g (l)) = \sum_{l = 1}^{m} 0$
180	36	olci	$⊢ ((1 \dots m) \subseteq ℤ_{\geq 1} \lor (1 \dots m) \in Fin)$
181		sumz	$⊢ ((1 \dots m) \subseteq ℤ_{\geq 1} \lor (1 \dots m) \in Fin) \to \sum_{l = 1}^{m} 0 = 0$
182	180 181	ax-mp	$⊢ \sum_{l = 1}^{m} 0 = 0$
183	179 182	eqtrdi	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to \sum_{l = 1}^{m} {vol}^{*} (g (l)) = 0$
184	167 183	breqtrd	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to {vol}^{*} (⋃_{l = 1}^{m} g (l)) \leq 0$
185		mblss	$⊢ g (l) \in dom vol \to g (l) \subseteq ℝ$
186	185	ralimi	$⊢ \forall l \in (1 \dots m) g (l) \in dom vol \to \forall l \in (1 \dots m) g (l) \subseteq ℝ$
187	52 186	syl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to \forall l \in (1 \dots m) g (l) \subseteq ℝ$
188		iunss	$⊢ ⋃_{l = 1}^{m} g (l) \subseteq ℝ \leftrightarrow \forall l \in (1 \dots m) g (l) \subseteq ℝ$
189	187 188	sylibr	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to ⋃_{l = 1}^{m} g (l) \subseteq ℝ$
190	189	adantr	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to ⋃_{l = 1}^{m} g (l) \subseteq ℝ$
191		ovolge0	$⊢ ⋃_{l = 1}^{m} g (l) \subseteq ℝ \to 0 \leq {vol}^{*} (⋃_{l = 1}^{m} g (l))$
192	190 191	syl	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to 0 \leq {vol}^{*} (⋃_{l = 1}^{m} g (l))$
193		ovolcl	$⊢ ⋃_{l = 1}^{m} g (l) \subseteq ℝ \to {vol}^{} (⋃_{l = 1}^{m} g (l)) \in ℝ^{}$
194	189 193	syl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to {vol}^{} (⋃_{l = 1}^{m} g (l)) \in ℝ^{}$
195	194	adantr	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to {vol}^{} (⋃_{l = 1}^{m} g (l)) \in ℝ^{}$
196		0xr	$⊢ 0 \in ℝ^{*}$
197		xrletri3	$⊢ ({vol}^{} (⋃_{l = 1}^{m} g (l)) \in ℝ^{} \land 0 \in ℝ^{}) \to ({vol}^{} (⋃_{l = 1}^{m} g (l)) = 0 \leftrightarrow ({vol}^{} (⋃_{l = 1}^{m} g (l)) \leq 0 \land 0 \leq {vol}^{} (⋃_{l = 1}^{m} g (l))))$
198	195 196 197	sylancl	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to ({vol}^{} (⋃_{l = 1}^{m} g (l)) = 0 \leftrightarrow ({vol}^{} (⋃_{l = 1}^{m} g (l)) \leq 0 \land 0 \leq {vol}^{*} (⋃_{l = 1}^{m} g (l))))$
199	184 192 198	mpbir2and	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to {vol}^{*} (⋃_{l = 1}^{m} g (l)) = 0$
200	139 199	eqtrd	$⊢ ((g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \land m \in ℕ) \to vol (⋃_{l = 1}^{m} g (l)) = 0$
201	200	mpteq2dva	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to (m \in ℕ ⟼ vol (⋃_{l = 1}^{m} g (l))) = (m \in ℕ ⟼ 0)$
202		fconstmpt	$⊢ ℕ \times \{0\} = (m \in ℕ ⟼ 0)$
203	201 202	eqtr4di	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to (m \in ℕ ⟼ vol (⋃_{l = 1}^{m} g (l))) = ℕ \times \{0\}$
204	137 203	eqtrd	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) = ℕ \times \{0\}$
205		frn	$⊢ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) : ℕ ⟶ dom vol \to ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \subseteq dom vol$
206		ffn	$⊢ vol : dom vol ⟶ [0, +∞] \to vol Fn dom vol$
207	133 206	ax-mp	$⊢ vol Fn dom vol$
208	119 62	fnmpti	$⊢ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) Fn ℕ$
209		fnco	$⊢ (vol Fn dom vol \land (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) Fn ℕ \land ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \subseteq dom vol) \to (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) Fn ℕ$
210	207 208 209	mp3an12	$⊢ ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) \subseteq dom vol \to (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) Fn ℕ$
211	56 205 210	3syl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) Fn ℕ$
212		1nn	$⊢ 1 \in ℕ$
213	212	ne0ii	$⊢ ℕ \neq \emptyset$
214		fconst5	$⊢ ((vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) Fn ℕ \land ℕ \neq \emptyset) \to (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) = ℕ \times \{0\} \leftrightarrow ran (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = \{0\})$
215	211 213 214	sylancl	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l)) = ℕ \times \{0\} \leftrightarrow ran (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = \{0\})$
216	204 215	mpbid	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to ran (vol \circ (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))) = \{0\}$
217	131 216	eqtr3id	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] = \{0\}$
218	217	supeq1d	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to sup (vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] ℝ^{} <) = sup (\{0\} ℝ^{} <)$
219		xrltso	$⊢ < Or ℝ^{*}$
220		supsn	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{}) \to sup (\{0\} ℝ^{*} <) = 0$
221	219 196 220	mp2an	$⊢ sup (\{0\} ℝ^{*} <) = 0$
222	218 221	eqtrdi	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to sup (vol [ran (m \in ℕ ⟼ ⋃_{l = 1}^{m} g (l))] ℝ^{*} <) = 0$
223	93 130 222	3eqtr3rd	$⊢ (g : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \in dom vol \land vol (x) = 0)) \to 0 = vol (⋃ A)$
224	223	ex	$⊢ g : ℕ \underset{onto}{⟶} A \to (\forall x \in A (x \in dom vol \land vol (x) = 0) \to 0 = vol (⋃ A))$
225	35 224	syl5	$⊢ g : ℕ \underset{onto}{⟶} A \to ((\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to 0 = vol (⋃ A))$
226	225	exlimiv	$⊢ \exists g g : ℕ \underset{onto}{⟶} A \to ((\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to 0 = vol (⋃ A))$
227	19 226	syl	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to ((\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to 0 = vol (⋃ A))$
228	227	expimpd	$⊢ A \neq \emptyset \to ((A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = vol (⋃ A))$
229	12 228	pm2.61ine	$⊢ (A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = vol (⋃ A)$
230		renepnf	$⊢ 0 \in ℝ \to 0 \neq +∞$
231	143 230	mp1i	$⊢ ⋃ A = ℝ \to 0 \neq +∞$
232		fveq2	$⊢ ⋃ A = ℝ \to vol (⋃ A) = vol (ℝ)$
233		rembl	$⊢ ℝ \in dom vol$
234		mblvol	$⊢ ℝ \in dom vol \to vol (ℝ) = {vol}^{*} (ℝ)$
235	233 234	ax-mp	$⊢ vol (ℝ) = {vol}^{*} (ℝ)$
236		ovolre	$⊢ {vol}^{*} (ℝ) = +∞$
237	235 236	eqtri	$⊢ vol (ℝ) = +∞$
238	232 237	eqtrdi	$⊢ ⋃ A = ℝ \to vol (⋃ A) = +∞$
239	231 238	neeqtrrd	$⊢ ⋃ A = ℝ \to 0 \neq vol (⋃ A)$
240	239	necon2i	$⊢ 0 = vol (⋃ A) \to ⋃ A \neq ℝ$
241	229 240	syl	$⊢ (A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to ⋃ A \neq ℝ$
242	241	expr	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to (⋃ A \subseteq ℝ \to ⋃ A \neq ℝ)$
243		eqimss	$⊢ ⋃ A = ℝ \to ⋃ A \subseteq ℝ$
244	243	necon3bi	$⊢ \neg ⋃ A \subseteq ℝ \to ⋃ A \neq ℝ$
245	242 244	pm2.61d1	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$

Metamath Proof Explorer

Theorem volsupnfl

Proof