ovolctb

Description: The volume of a denumerable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

		Ref	Expression
	Assertion	ovolctb	$⊢ (A \subseteq ℝ \land A \approx ℕ) \to {vol}^{*} (A) = 0$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ ℕ \approx A \leftrightarrow \exists f f : ℕ \underset{1-1 onto}{⟶} A$
2		simpll	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to A \subseteq ℝ$
3		f1of	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to f : ℕ ⟶ A$
4	3	adantl	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to f : ℕ ⟶ A$
5	4	ffvelrnda	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to f (x) \in A$
6	2 5	sseldd	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to f (x) \in ℝ$
7	6	leidd	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to f (x) \leq f (x)$
8		df-br	$⊢ f (x) \leq f (x) \leftrightarrow ⟨f (x), f (x)⟩ \in \leq$
9	7 8	sylib	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to ⟨f (x), f (x)⟩ \in \leq$
10	6 6	opelxpd	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to ⟨f (x), f (x)⟩ \in ℝ^{2}$
11	9 10	elind	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to ⟨f (x), f (x)⟩ \in (\leq \cap ℝ^{2})$
12		df-ov	$⊢ f (x) I f (x) = I (⟨f (x), f (x)⟩)$
13		opex	$⊢ ⟨f (x), f (x)⟩ \in V$
14		fvi	$⊢ ⟨f (x), f (x)⟩ \in V \to I (⟨f (x), f (x)⟩) = ⟨f (x), f (x)⟩$
15	13 14	ax-mp	$⊢ I (⟨f (x), f (x)⟩) = ⟨f (x), f (x)⟩$
16	12 15	eqtri	$⊢ f (x) I f (x) = ⟨f (x), f (x)⟩$
17	16	mpteq2i	$⊢ (x \in ℕ ⟼ f (x) I f (x)) = (x \in ℕ ⟼ ⟨f (x), f (x)⟩)$
18	11 17	fmptd	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (x \in ℕ ⟼ f (x) I f (x)) : ℕ ⟶ \leq \cap ℝ^{2}$
19		nnex	$⊢ ℕ \in V$
20	19	a1i	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to ℕ \in V$
21	6	recnd	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to f (x) \in ℂ$
22	4	feqmptd	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to f = (x \in ℕ ⟼ f (x))$
23	20 21 21 22 22	offval2	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to f I_{f} f = (x \in ℕ ⟼ f (x) I f (x))$
24	23	feq1d	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to ((f I_{f} f) : ℕ ⟶ \leq \cap ℝ^{2} \leftrightarrow (x \in ℕ ⟼ f (x) I f (x)) : ℕ ⟶ \leq \cap ℝ^{2})$
25	18 24	mpbird	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (f I_{f} f) : ℕ ⟶ \leq \cap ℝ^{2}$
26		f1ofo	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to f : ℕ \underset{onto}{⟶} A$
27	26	adantl	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to f : ℕ \underset{onto}{⟶} A$
28		forn	$⊢ f : ℕ \underset{onto}{⟶} A \to ran f = A$
29	27 28	syl	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to ran f = A$
30	29	eleq2d	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (y \in ran f \leftrightarrow y \in A)$
31		f1ofn	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to f Fn ℕ$
32	31	adantl	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to f Fn ℕ$
33		fvelrnb	$⊢ f Fn ℕ \to (y \in ran f \leftrightarrow \exists x \in ℕ f (x) = y)$
34	32 33	syl	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (y \in ran f \leftrightarrow \exists x \in ℕ f (x) = y)$
35	30 34	bitr3d	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (y \in A \leftrightarrow \exists x \in ℕ f (x) = y)$
36	23 17	syl6eq	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to f I_{f} f = (x \in ℕ ⟼ ⟨f (x), f (x)⟩)$
37	36	fveq1d	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (f I_{f} f) (x) = (x \in ℕ ⟼ ⟨f (x), f (x)⟩) (x)$
38		eqid	$⊢ (x \in ℕ ⟼ ⟨f (x), f (x)⟩) = (x \in ℕ ⟼ ⟨f (x), f (x)⟩)$
39	38	fvmpt2	$⊢ (x \in ℕ \land ⟨f (x), f (x)⟩ \in V) \to (x \in ℕ ⟼ ⟨f (x), f (x)⟩) (x) = ⟨f (x), f (x)⟩$
40	13 39	mpan2	$⊢ x \in ℕ \to (x \in ℕ ⟼ ⟨f (x), f (x)⟩) (x) = ⟨f (x), f (x)⟩$
41	37 40	sylan9eq	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to (f I_{f} f) (x) = ⟨f (x), f (x)⟩$
42	41	fveq2d	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to 1^{st} ((f I_{f} f) (x)) = 1^{st} (⟨f (x), f (x)⟩)$
43		fvex	$⊢ f (x) \in V$
44	43 43	op1st	$⊢ 1^{st} (⟨f (x), f (x)⟩) = f (x)$
45	42 44	syl6eq	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to 1^{st} ((f I_{f} f) (x)) = f (x)$
46	45 7	eqbrtrd	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to 1^{st} ((f I_{f} f) (x)) \leq f (x)$
47	41	fveq2d	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to 2^{nd} ((f I_{f} f) (x)) = 2^{nd} (⟨f (x), f (x)⟩)$
48	43 43	op2nd	$⊢ 2^{nd} (⟨f (x), f (x)⟩) = f (x)$
49	47 48	syl6eq	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to 2^{nd} ((f I_{f} f) (x)) = f (x)$
50	7 49	breqtrrd	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to f (x) \leq 2^{nd} ((f I_{f} f) (x))$
51	46 50	jca	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to (1^{st} ((f I_{f} f) (x)) \leq f (x) \land f (x) \leq 2^{nd} ((f I_{f} f) (x)))$
52		breq2	$⊢ f (x) = y \to (1^{st} ((f I_{f} f) (x)) \leq f (x) \leftrightarrow 1^{st} ((f I_{f} f) (x)) \leq y)$
53		breq1	$⊢ f (x) = y \to (f (x) \leq 2^{nd} ((f I_{f} f) (x)) \leftrightarrow y \leq 2^{nd} ((f I_{f} f) (x)))$
54	52 53	anbi12d	$⊢ f (x) = y \to ((1^{st} ((f I_{f} f) (x)) \leq f (x) \land f (x) \leq 2^{nd} ((f I_{f} f) (x))) \leftrightarrow (1^{st} ((f I_{f} f) (x)) \leq y \land y \leq 2^{nd} ((f I_{f} f) (x))))$
55	51 54	syl5ibcom	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to (f (x) = y \to (1^{st} ((f I_{f} f) (x)) \leq y \land y \leq 2^{nd} ((f I_{f} f) (x))))$
56	55	reximdva	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (\exists x \in ℕ f (x) = y \to \exists x \in ℕ (1^{st} ((f I_{f} f) (x)) \leq y \land y \leq 2^{nd} ((f I_{f} f) (x))))$
57	35 56	sylbid	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (y \in A \to \exists x \in ℕ (1^{st} ((f I_{f} f) (x)) \leq y \land y \leq 2^{nd} ((f I_{f} f) (x))))$
58	57	ralrimiv	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to \forall y \in A \exists x \in ℕ (1^{st} ((f I_{f} f) (x)) \leq y \land y \leq 2^{nd} ((f I_{f} f) (x)))$
59		ovolficc	$⊢ (A \subseteq ℝ \land (f I_{f} f) : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ([.] \circ (f I_{f} f)) \leftrightarrow \forall y \in A \exists x \in ℕ (1^{st} ((f I_{f} f) (x)) \leq y \land y \leq 2^{nd} ((f I_{f} f) (x))))$
60	25 59	syldan	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (A \subseteq ⋃ ran ([.] \circ (f I_{f} f)) \leftrightarrow \forall y \in A \exists x \in ℕ (1^{st} ((f I_{f} f) (x)) \leq y \land y \leq 2^{nd} ((f I_{f} f) (x))))$
61	58 60	mpbird	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to A \subseteq ⋃ ran ([.] \circ (f I_{f} f))$
62		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) = seq 1 (+ ((abs \circ -) \circ (f I_{f} f)))$
63	62	ovollb2	$⊢ ((f I_{f} f) : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ (f I_{f} f))) \to {vol}^{} (A) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) ℝ^{} <)$
64	25 61 63	syl2anc	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to {vol}^{} (A) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) ℝ^{} <)$
65	21 21	opelxpd	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to ⟨f (x), f (x)⟩ \in (ℂ \times ℂ)$
66		absf	$⊢ abs : ℂ ⟶ ℝ$
67		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
68		fco	$⊢ (abs : ℂ ⟶ ℝ \land - : ℂ \times ℂ ⟶ ℂ) \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
69	66 67 68	mp2an	$⊢ (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
70	69	a1i	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
71	70	feqmptd	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to abs \circ - = (y \in (ℂ \times ℂ) ⟼ (abs \circ -) (y))$
72		fveq2	$⊢ y = ⟨f (x), f (x)⟩ \to (abs \circ -) (y) = (abs \circ -) (⟨f (x), f (x)⟩)$
73		df-ov	$⊢ f (x) (abs \circ -) f (x) = (abs \circ -) (⟨f (x), f (x)⟩)$
74	72 73	syl6eqr	$⊢ y = ⟨f (x), f (x)⟩ \to (abs \circ -) (y) = f (x) (abs \circ -) f (x)$
75	65 36 71 74	fmptco	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (abs \circ -) \circ (f I_{f} f) = (x \in ℕ ⟼ f (x) (abs \circ -) f (x))$
76		cnmet	$⊢ abs \circ - \in Met (ℂ)$
77		met0	$⊢ (abs \circ - \in Met (ℂ) \land f (x) \in ℂ) \to f (x) (abs \circ -) f (x) = 0$
78	76 21 77	sylancr	$⊢ ((A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \land x \in ℕ) \to f (x) (abs \circ -) f (x) = 0$
79	78	mpteq2dva	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (x \in ℕ ⟼ f (x) (abs \circ -) f (x)) = (x \in ℕ ⟼ 0)$
80	75 79	eqtrd	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (abs \circ -) \circ (f I_{f} f) = (x \in ℕ ⟼ 0)$
81		fconstmpt	$⊢ ℕ \times \{0\} = (x \in ℕ ⟼ 0)$
82	80 81	syl6eqr	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to (abs \circ -) \circ (f I_{f} f) = ℕ \times \{0\}$
83	82	seqeq3d	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) = seq 1 (+ (ℕ \times \{0\}))$
84		1z	$⊢ 1 \in ℤ$
85		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
86	85	ser0f	$⊢ 1 \in ℤ \to seq 1 (+ (ℕ \times \{0\})) = ℕ \times \{0\}$
87	84 86	ax-mp	$⊢ seq 1 (+ (ℕ \times \{0\})) = ℕ \times \{0\}$
88	83 87	syl6eq	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) = ℕ \times \{0\}$
89	88	rneqd	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to ran seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) = ran (ℕ \times \{0\})$
90		1nn	$⊢ 1 \in ℕ$
91		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
92		rnxp	$⊢ ℕ \neq \emptyset \to ran (ℕ \times \{0\}) = \{0\}$
93	90 91 92	mp2b	$⊢ ran (ℕ \times \{0\}) = \{0\}$
94	89 93	syl6eq	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to ran seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) = \{0\}$
95	94	supeq1d	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to sup (ran seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) ℝ^{} <) = sup (\{0\} ℝ^{} <)$
96		xrltso	$⊢ < Or ℝ^{*}$
97		0xr	$⊢ 0 \in ℝ^{*}$
98		supsn	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{}) \to sup (\{0\} ℝ^{*} <) = 0$
99	96 97 98	mp2an	$⊢ sup (\{0\} ℝ^{*} <) = 0$
100	95 99	syl6eq	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to sup (ran seq 1 (+ ((abs \circ -) \circ (f I_{f} f))) ℝ^{*} <) = 0$
101	64 100	breqtrd	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to {vol}^{*} (A) \leq 0$
102		ovolge0	$⊢ A \subseteq ℝ \to 0 \leq {vol}^{*} (A)$
103	102	adantr	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to 0 \leq {vol}^{*} (A)$
104		ovolcl	$⊢ A \subseteq ℝ \to {vol}^{} (A) \in ℝ^{}$
105	104	adantr	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to {vol}^{} (A) \in ℝ^{}$
106		xrletri3	$⊢ ({vol}^{} (A) \in ℝ^{} \land 0 \in ℝ^{}) \to ({vol}^{} (A) = 0 \leftrightarrow ({vol}^{} (A) \leq 0 \land 0 \leq {vol}^{} (A)))$
107	105 97 106	sylancl	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to ({vol}^{} (A) = 0 \leftrightarrow ({vol}^{} (A) \leq 0 \land 0 \leq {vol}^{*} (A)))$
108	101 103 107	mpbir2and	$⊢ (A \subseteq ℝ \land f : ℕ \underset{1-1 onto}{⟶} A) \to {vol}^{*} (A) = 0$
109	108	ex	$⊢ A \subseteq ℝ \to (f : ℕ \underset{1-1 onto}{⟶} A \to {vol}^{*} (A) = 0)$
110	109	exlimdv	$⊢ A \subseteq ℝ \to (\exists f f : ℕ \underset{1-1 onto}{⟶} A \to {vol}^{*} (A) = 0)$
111	1 110	syl5bi	$⊢ A \subseteq ℝ \to (ℕ \approx A \to {vol}^{*} (A) = 0)$
112		ensym	$⊢ A \approx ℕ \to ℕ \approx A$
113	111 112	impel	$⊢ (A \subseteq ℝ \land A \approx ℕ) \to {vol}^{*} (A) = 0$

Metamath Proof Explorer

Theorem ovolctb

Proof