vitalilem5

	Ref	Expression
Hypotheses	vitali.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ)\}$
	vitali.2	$⊢ S = [0, 1] / \underset{˙}{\sim}$
	vitali.3	$⊢ φ \to F Fn S$
	vitali.4	$⊢ φ \to \forall z \in S (z \neq \emptyset \to F (z) \in z)$
	vitali.5	$⊢ φ \to G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
	vitali.6	$⊢ T = (n \in ℕ ⟼ \{s \in ℝ \| s - G (n) \in ran F\})$
	vitali.7	$⊢ φ \to \neg ran F \in (𝒫 ℝ ∖ dom vol)$
Assertion	vitalilem5	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		vitali.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ)\}$
2		vitali.2	$⊢ S = [0, 1] / \underset{˙}{\sim}$
3		vitali.3	$⊢ φ \to F Fn S$
4		vitali.4	$⊢ φ \to \forall z \in S (z \neq \emptyset \to F (z) \in z)$
5		vitali.5	$⊢ φ \to G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
6		vitali.6	$⊢ T = (n \in ℕ ⟼ \{s \in ℝ \| s - G (n) \in ran F\})$
7		vitali.7	$⊢ φ \to \neg ran F \in (𝒫 ℝ ∖ dom vol)$
8		0lt1	$⊢ 0 < 1$
9		0re	$⊢ 0 \in ℝ$
10		1re	$⊢ 1 \in ℝ$
11		0le1	$⊢ 0 \leq 1$
12		ovolicc	$⊢ (0 \in ℝ \land 1 \in ℝ \land 0 \leq 1) \to {vol}^{*} ([0, 1]) = 1 - 0$
13	9 10 11 12	mp3an	$⊢ {vol}^{*} ([0, 1]) = 1 - 0$
14		1m0e1	$⊢ 1 - 0 = 1$
15	13 14	eqtri	$⊢ {vol}^{*} ([0, 1]) = 1$
16	8 15	breqtrri	$⊢ 0 < {vol}^{*} ([0, 1])$
17	15 10	eqeltri	$⊢ {vol}^{*} ([0, 1]) \in ℝ$
18	9 17	ltnlei	$⊢ 0 < {vol}^{} ([0, 1]) \leftrightarrow \neg {vol}^{} ([0, 1]) \leq 0$
19	16 18	mpbi	$⊢ \neg {vol}^{*} ([0, 1]) \leq 0$
20	1 2 3 4 5 6 7	vitalilem2	$⊢ φ \to (ran F \subseteq [0, 1] \land [0, 1] \subseteq ⋃_{m \in ℕ} T (m) \land ⋃_{m \in ℕ} T (m) \subseteq [- 1, 2])$
21	20	simp2d	$⊢ φ \to [0, 1] \subseteq ⋃_{m \in ℕ} T (m)$
22	1	vitalilem1	$⊢ \underset{˙}{\sim} Er [0, 1]$
23		erdm	$⊢ \underset{˙}{\sim} Er [0, 1] \to dom \underset{˙}{\sim} = [0, 1]$
24	22 23	ax-mp	$⊢ dom \underset{˙}{\sim} = [0, 1]$
25		simpr	$⊢ (φ \land z \in S) \to z \in S$
26	25 2	eleqtrdi	$⊢ (φ \land z \in S) \to z \in ([0, 1] / \underset{˙}{\sim})$
27		elqsn0	$⊢ (dom \underset{˙}{\sim} = [0, 1] \land z \in ([0, 1] / \underset{˙}{\sim})) \to z \neq \emptyset$
28	24 26 27	sylancr	$⊢ (φ \land z \in S) \to z \neq \emptyset$
29	22	a1i	$⊢ φ \to \underset{˙}{\sim} Er [0, 1]$
30	29	qsss	$⊢ φ \to [0, 1] / \underset{˙}{\sim} \subseteq 𝒫 [0, 1]$
31	2 30	eqsstrid	$⊢ φ \to S \subseteq 𝒫 [0, 1]$
32	31	sselda	$⊢ (φ \land z \in S) \to z \in 𝒫 [0, 1]$
33	32	elpwid	$⊢ (φ \land z \in S) \to z \subseteq [0, 1]$
34	33	sseld	$⊢ (φ \land z \in S) \to (F (z) \in z \to F (z) \in [0, 1])$
35	28 34	embantd	$⊢ (φ \land z \in S) \to ((z \neq \emptyset \to F (z) \in z) \to F (z) \in [0, 1])$
36	35	ralimdva	$⊢ φ \to (\forall z \in S (z \neq \emptyset \to F (z) \in z) \to \forall z \in S F (z) \in [0, 1])$
37	4 36	mpd	$⊢ φ \to \forall z \in S F (z) \in [0, 1]$
38		ffnfv	$⊢ F : S ⟶ [0, 1] \leftrightarrow (F Fn S \land \forall z \in S F (z) \in [0, 1])$
39	3 37 38	sylanbrc	$⊢ φ \to F : S ⟶ [0, 1]$
40	39	frnd	$⊢ φ \to ran F \subseteq [0, 1]$
41		unitssre	$⊢ [0, 1] \subseteq ℝ$
42	40 41	sstrdi	$⊢ φ \to ran F \subseteq ℝ$
43		reex	$⊢ ℝ \in V$
44	43	elpw2	$⊢ ran F \in 𝒫 ℝ \leftrightarrow ran F \subseteq ℝ$
45	42 44	sylibr	$⊢ φ \to ran F \in 𝒫 ℝ$
46	45	anim1i	$⊢ (φ \land \neg ran F \in dom vol) \to (ran F \in 𝒫 ℝ \land \neg ran F \in dom vol)$
47		eldif	$⊢ ran F \in (𝒫 ℝ ∖ dom vol) \leftrightarrow (ran F \in 𝒫 ℝ \land \neg ran F \in dom vol)$
48	46 47	sylibr	$⊢ (φ \land \neg ran F \in dom vol) \to ran F \in (𝒫 ℝ ∖ dom vol)$
49	48	ex	$⊢ φ \to (\neg ran F \in dom vol \to ran F \in (𝒫 ℝ ∖ dom vol))$
50	7 49	mt3d	$⊢ φ \to ran F \in dom vol$
51		f1of	$⊢ G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
52	5 51	syl	$⊢ φ \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
53		inss1	$⊢ ℚ \cap [- 1, 1] \subseteq ℚ$
54		qssre	$⊢ ℚ \subseteq ℝ$
55	53 54	sstri	$⊢ ℚ \cap [- 1, 1] \subseteq ℝ$
56		fss	$⊢ (G : ℕ ⟶ ℚ \cap [- 1, 1] \land ℚ \cap [- 1, 1] \subseteq ℝ) \to G : ℕ ⟶ ℝ$
57	52 55 56	sylancl	$⊢ φ \to G : ℕ ⟶ ℝ$
58	57	ffvelrnda	$⊢ (φ \land n \in ℕ) \to G (n) \in ℝ$
59		shftmbl	$⊢ (ran F \in dom vol \land G (n) \in ℝ) \to \{s \in ℝ \| s - G (n) \in ran F\} \in dom vol$
60	50 58 59	syl2an2r	$⊢ (φ \land n \in ℕ) \to \{s \in ℝ \| s - G (n) \in ran F\} \in dom vol$
61	60 6	fmptd	$⊢ φ \to T : ℕ ⟶ dom vol$
62	61	ffvelrnda	$⊢ (φ \land m \in ℕ) \to T (m) \in dom vol$
63	62	ralrimiva	$⊢ φ \to \forall m \in ℕ T (m) \in dom vol$
64		iunmbl	$⊢ \forall m \in ℕ T (m) \in dom vol \to ⋃_{m \in ℕ} T (m) \in dom vol$
65	63 64	syl	$⊢ φ \to ⋃_{m \in ℕ} T (m) \in dom vol$
66		mblss	$⊢ ⋃_{m \in ℕ} T (m) \in dom vol \to ⋃_{m \in ℕ} T (m) \subseteq ℝ$
67	65 66	syl	$⊢ φ \to ⋃_{m \in ℕ} T (m) \subseteq ℝ$
68		ovolss	$⊢ ([0, 1] \subseteq ⋃_{m \in ℕ} T (m) \land ⋃_{m \in ℕ} T (m) \subseteq ℝ) \to {vol}^{} ([0, 1]) \leq {vol}^{} (⋃_{m \in ℕ} T (m))$
69	21 67 68	syl2anc	$⊢ φ \to {vol}^{} ([0, 1]) \leq {vol}^{} (⋃_{m \in ℕ} T (m))$
70		eqid	$⊢ seq 1 (+ (m \in ℕ ⟼ {vol}^{} (T (m)))) = seq 1 (+ (m \in ℕ ⟼ {vol}^{} (T (m))))$
71		eqid	$⊢ (m \in ℕ ⟼ {vol}^{} (T (m))) = (m \in ℕ ⟼ {vol}^{} (T (m)))$
72		mblss	$⊢ T (m) \in dom vol \to T (m) \subseteq ℝ$
73	62 72	syl	$⊢ (φ \land m \in ℕ) \to T (m) \subseteq ℝ$
74	1 2 3 4 5 6 7	vitalilem4	$⊢ (φ \land m \in ℕ) \to {vol}^{*} (T (m)) = 0$
75	74 9	eqeltrdi	$⊢ (φ \land m \in ℕ) \to {vol}^{*} (T (m)) \in ℝ$
76	74	mpteq2dva	$⊢ φ \to (m \in ℕ ⟼ {vol}^{*} (T (m))) = (m \in ℕ ⟼ 0)$
77		fconstmpt	$⊢ ℕ \times \{0\} = (m \in ℕ ⟼ 0)$
78		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
79	78	xpeq1i	$⊢ ℕ \times \{0\} = ℤ_{\geq 1} \times \{0\}$
80	77 79	eqtr3i	$⊢ (m \in ℕ ⟼ 0) = ℤ_{\geq 1} \times \{0\}$
81	76 80	syl6eq	$⊢ φ \to (m \in ℕ ⟼ {vol}^{*} (T (m))) = ℤ_{\geq 1} \times \{0\}$
82	81	seqeq3d	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ {vol}^{*} (T (m)))) = seq 1 (+ (ℤ_{\geq 1} \times \{0\}))$
83		1z	$⊢ 1 \in ℤ$
84		serclim0	$⊢ 1 \in ℤ \to seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ 0$
85	83 84	ax-mp	$⊢ seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ 0$
86	82 85	eqbrtrdi	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ {vol}^{*} (T (m)))) ⇝ 0$
87		seqex	$⊢ seq 1 (+ (m \in ℕ ⟼ {vol}^{*} (T (m)))) \in V$
88		c0ex	$⊢ 0 \in V$
89	87 88	breldm	$⊢ seq 1 (+ (m \in ℕ ⟼ {vol}^{} (T (m)))) ⇝ 0 \to seq 1 (+ (m \in ℕ ⟼ {vol}^{} (T (m)))) \in dom ⇝$
90	86 89	syl	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ {vol}^{*} (T (m)))) \in dom ⇝$
91	70 71 73 75 90	ovoliun2	$⊢ φ \to {vol}^{} (⋃_{m \in ℕ} T (m)) \leq \sum_{m \in ℕ} {vol}^{} (T (m))$
92	74	sumeq2dv	$⊢ φ \to \sum_{m \in ℕ} {vol}^{*} (T (m)) = \sum_{m \in ℕ} 0$
93	78	eqimssi	$⊢ ℕ \subseteq ℤ_{\geq 1}$
94	93	orci	$⊢ (ℕ \subseteq ℤ_{\geq 1} \lor ℕ \in Fin)$
95		sumz	$⊢ (ℕ \subseteq ℤ_{\geq 1} \lor ℕ \in Fin) \to \sum_{m \in ℕ} 0 = 0$
96	94 95	ax-mp	$⊢ \sum_{m \in ℕ} 0 = 0$
97	92 96	syl6eq	$⊢ φ \to \sum_{m \in ℕ} {vol}^{*} (T (m)) = 0$
98	91 97	breqtrd	$⊢ φ \to {vol}^{*} (⋃_{m \in ℕ} T (m)) \leq 0$
99		ovolge0	$⊢ ⋃_{m \in ℕ} T (m) \subseteq ℝ \to 0 \leq {vol}^{*} (⋃_{m \in ℕ} T (m))$
100	67 99	syl	$⊢ φ \to 0 \leq {vol}^{*} (⋃_{m \in ℕ} T (m))$
101		ovolcl	$⊢ ⋃_{m \in ℕ} T (m) \subseteq ℝ \to {vol}^{} (⋃_{m \in ℕ} T (m)) \in ℝ^{}$
102	67 101	syl	$⊢ φ \to {vol}^{} (⋃_{m \in ℕ} T (m)) \in ℝ^{}$
103		0xr	$⊢ 0 \in ℝ^{*}$
104		xrletri3	$⊢ ({vol}^{} (⋃_{m \in ℕ} T (m)) \in ℝ^{} \land 0 \in ℝ^{}) \to ({vol}^{} (⋃_{m \in ℕ} T (m)) = 0 \leftrightarrow ({vol}^{} (⋃_{m \in ℕ} T (m)) \leq 0 \land 0 \leq {vol}^{} (⋃_{m \in ℕ} T (m))))$
105	102 103 104	sylancl	$⊢ φ \to ({vol}^{} (⋃_{m \in ℕ} T (m)) = 0 \leftrightarrow ({vol}^{} (⋃_{m \in ℕ} T (m)) \leq 0 \land 0 \leq {vol}^{*} (⋃_{m \in ℕ} T (m))))$
106	98 100 105	mpbir2and	$⊢ φ \to {vol}^{*} (⋃_{m \in ℕ} T (m)) = 0$
107	69 106	breqtrd	$⊢ φ \to {vol}^{*} ([0, 1]) \leq 0$
108	19 107	mto	$⊢ \neg φ$

Metamath Proof Explorer

Theorem vitalilem5

Proof