vitalilem2

	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	vitalilem2	$⊢ φ \to (ran F \subseteq [0, 1] \land [0, 1] \subseteq ⋃_{m \in ℕ} T (m) \land ⋃_{m \in ℕ} T (m) \subseteq [- 1, 2])$

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		neeq1	$⊢ [v] \underset{˙}{\sim} = z \to ([v] \underset{˙}{\sim} \neq \emptyset \leftrightarrow z \neq \emptyset)$
9	1	vitalilem1	$⊢ \underset{˙}{\sim} Er [0, 1]$
10		erdm	$⊢ \underset{˙}{\sim} Er [0, 1] \to dom \underset{˙}{\sim} = [0, 1]$
11	9 10	ax-mp	$⊢ dom \underset{˙}{\sim} = [0, 1]$
12	11	eleq2i	$⊢ v \in dom \underset{˙}{\sim} \leftrightarrow v \in [0, 1]$
13		ecdmn0	$⊢ v \in dom \underset{˙}{\sim} \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset$
14	12 13	bitr3i	$⊢ v \in [0, 1] \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset$
15	14	biimpi	$⊢ v \in [0, 1] \to [v] \underset{˙}{\sim} \neq \emptyset$
16	2 8 15	ectocl	$⊢ z \in S \to z \neq \emptyset$
17	16	adantl	$⊢ (φ \land z \in S) \to z \neq \emptyset$
18		sseq1	$⊢ [w] \underset{˙}{\sim} = z \to ([w] \underset{˙}{\sim} \subseteq [0, 1] \leftrightarrow z \subseteq [0, 1])$
19	9	a1i	$⊢ w \in [0, 1] \to \underset{˙}{\sim} Er [0, 1]$
20	19	ecss	$⊢ w \in [0, 1] \to [w] \underset{˙}{\sim} \subseteq [0, 1]$
21	2 18 20	ectocl	$⊢ z \in S \to z \subseteq [0, 1]$
22	21	adantl	$⊢ (φ \land z \in S) \to z \subseteq [0, 1]$
23	22	sseld	$⊢ (φ \land z \in S) \to (F (z) \in z \to F (z) \in [0, 1])$
24	17 23	embantd	$⊢ (φ \land z \in S) \to ((z \neq \emptyset \to F (z) \in z) \to F (z) \in [0, 1])$
25	24	ralimdva	$⊢ φ \to (\forall z \in S (z \neq \emptyset \to F (z) \in z) \to \forall z \in S F (z) \in [0, 1])$
26	4 25	mpd	$⊢ φ \to \forall z \in S F (z) \in [0, 1]$
27		ffnfv	$⊢ F : S ⟶ [0, 1] \leftrightarrow (F Fn S \land \forall z \in S F (z) \in [0, 1])$
28	3 26 27	sylanbrc	$⊢ φ \to F : S ⟶ [0, 1]$
29	28	frnd	$⊢ φ \to ran F \subseteq [0, 1]$
30	5	adantr	$⊢ (φ \land v \in [0, 1]) \to G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
31		f1ocnv	$⊢ G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to G^{-1} : ℚ \cap [- 1, 1] \underset{1-1 onto}{⟶} ℕ$
32		f1of	$⊢ G^{-1} : ℚ \cap [- 1, 1] \underset{1-1 onto}{⟶} ℕ \to G^{-1} : ℚ \cap [- 1, 1] ⟶ ℕ$
33	30 31 32	3syl	$⊢ (φ \land v \in [0, 1]) \to G^{-1} : ℚ \cap [- 1, 1] ⟶ ℕ$
34		simpr	$⊢ (φ \land v \in [0, 1]) \to v \in [0, 1]$
35	34 14	sylib	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} \neq \emptyset$
36		neeq1	$⊢ z = [v] \underset{˙}{\sim} \to (z \neq \emptyset \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset)$
37		fveq2	$⊢ z = [v] \underset{˙}{\sim} \to F (z) = F ([v] \underset{˙}{\sim})$
38		id	$⊢ z = [v] \underset{˙}{\sim} \to z = [v] \underset{˙}{\sim}$
39	37 38	eleq12d	$⊢ z = [v] \underset{˙}{\sim} \to (F (z) \in z \leftrightarrow F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim})$
40	36 39	imbi12d	$⊢ z = [v] \underset{˙}{\sim} \to ((z \neq \emptyset \to F (z) \in z) \leftrightarrow ([v] \underset{˙}{\sim} \neq \emptyset \to F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim}))$
41	4	adantr	$⊢ (φ \land v \in [0, 1]) \to \forall z \in S (z \neq \emptyset \to F (z) \in z)$
42		ovex	$⊢ [0, 1] \in V$
43		erex	$⊢ \underset{˙}{\sim} Er [0, 1] \to ([0, 1] \in V \to \underset{˙}{\sim} \in V)$
44	9 42 43	mp2	$⊢ \underset{˙}{\sim} \in V$
45	44	ecelqsi	$⊢ v \in [0, 1] \to [v] \underset{˙}{\sim} \in ([0, 1] / \underset{˙}{\sim})$
46	45	adantl	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} \in ([0, 1] / \underset{˙}{\sim})$
47	46 2	eleqtrrdi	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} \in S$
48	40 41 47	rspcdva	$⊢ (φ \land v \in [0, 1]) \to ([v] \underset{˙}{\sim} \neq \emptyset \to F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim})$
49	35 48	mpd	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim}$
50		fvex	$⊢ F ([v] \underset{˙}{\sim}) \in V$
51		vex	$⊢ v \in V$
52	50 51	elec	$⊢ F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim} \leftrightarrow v \underset{˙}{\sim} F ([v] \underset{˙}{\sim})$
53		oveq12	$⊢ (x = v \land y = F ([v] \underset{˙}{\sim})) \to x - y = v - F ([v] \underset{˙}{\sim})$
54	53	eleq1d	$⊢ (x = v \land y = F ([v] \underset{˙}{\sim})) \to (x - y \in ℚ \leftrightarrow v - F ([v] \underset{˙}{\sim}) \in ℚ)$
55	54 1	brab2a	$⊢ v \underset{˙}{\sim} F ([v] \underset{˙}{\sim}) \leftrightarrow ((v \in [0, 1] \land F ([v] \underset{˙}{\sim}) \in [0, 1]) \land v - F ([v] \underset{˙}{\sim}) \in ℚ)$
56	52 55	bitri	$⊢ F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim} \leftrightarrow ((v \in [0, 1] \land F ([v] \underset{˙}{\sim}) \in [0, 1]) \land v - F ([v] \underset{˙}{\sim}) \in ℚ)$
57	49 56	sylib	$⊢ (φ \land v \in [0, 1]) \to ((v \in [0, 1] \land F ([v] \underset{˙}{\sim}) \in [0, 1]) \land v - F ([v] \underset{˙}{\sim}) \in ℚ)$
58	57	simprd	$⊢ (φ \land v \in [0, 1]) \to v - F ([v] \underset{˙}{\sim}) \in ℚ$
59		elicc01	$⊢ v \in [0, 1] \leftrightarrow (v \in ℝ \land 0 \leq v \land v \leq 1)$
60	34 59	sylib	$⊢ (φ \land v \in [0, 1]) \to (v \in ℝ \land 0 \leq v \land v \leq 1)$
61	60	simp1d	$⊢ (φ \land v \in [0, 1]) \to v \in ℝ$
62	57	simpld	$⊢ (φ \land v \in [0, 1]) \to (v \in [0, 1] \land F ([v] \underset{˙}{\sim}) \in [0, 1])$
63	62	simprd	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \in [0, 1]$
64		elicc01	$⊢ F ([v] \underset{˙}{\sim}) \in [0, 1] \leftrightarrow (F ([v] \underset{˙}{\sim}) \in ℝ \land 0 \leq F ([v] \underset{˙}{\sim}) \land F ([v] \underset{˙}{\sim}) \leq 1)$
65	63 64	sylib	$⊢ (φ \land v \in [0, 1]) \to (F ([v] \underset{˙}{\sim}) \in ℝ \land 0 \leq F ([v] \underset{˙}{\sim}) \land F ([v] \underset{˙}{\sim}) \leq 1)$
66	65	simp1d	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \in ℝ$
67	61 66	resubcld	$⊢ (φ \land v \in [0, 1]) \to v - F ([v] \underset{˙}{\sim}) \in ℝ$
68	66 61	resubcld	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) - v \in ℝ$
69		1red	$⊢ (φ \land v \in [0, 1]) \to 1 \in ℝ$
70	60	simp2d	$⊢ (φ \land v \in [0, 1]) \to 0 \leq v$
71	66 61	subge02d	$⊢ (φ \land v \in [0, 1]) \to (0 \leq v \leftrightarrow F ([v] \underset{˙}{\sim}) - v \leq F ([v] \underset{˙}{\sim}))$
72	70 71	mpbid	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) - v \leq F ([v] \underset{˙}{\sim})$
73	65	simp3d	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \leq 1$
74	68 66 69 72 73	letrd	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) - v \leq 1$
75	68 69	lenegd	$⊢ (φ \land v \in [0, 1]) \to (F ([v] \underset{˙}{\sim}) - v \leq 1 \leftrightarrow - 1 \leq - (F ([v] \underset{˙}{\sim}) - v))$
76	74 75	mpbid	$⊢ (φ \land v \in [0, 1]) \to - 1 \leq - (F ([v] \underset{˙}{\sim}) - v)$
77	66	recnd	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \in ℂ$
78	61	recnd	$⊢ (φ \land v \in [0, 1]) \to v \in ℂ$
79	77 78	negsubdi2d	$⊢ (φ \land v \in [0, 1]) \to - (F ([v] \underset{˙}{\sim}) - v) = v - F ([v] \underset{˙}{\sim})$
80	76 79	breqtrd	$⊢ (φ \land v \in [0, 1]) \to - 1 \leq v - F ([v] \underset{˙}{\sim})$
81	65	simp2d	$⊢ (φ \land v \in [0, 1]) \to 0 \leq F ([v] \underset{˙}{\sim})$
82	61 66	subge02d	$⊢ (φ \land v \in [0, 1]) \to (0 \leq F ([v] \underset{˙}{\sim}) \leftrightarrow v - F ([v] \underset{˙}{\sim}) \leq v)$
83	81 82	mpbid	$⊢ (φ \land v \in [0, 1]) \to v - F ([v] \underset{˙}{\sim}) \leq v$
84	60	simp3d	$⊢ (φ \land v \in [0, 1]) \to v \leq 1$
85	67 61 69 83 84	letrd	$⊢ (φ \land v \in [0, 1]) \to v - F ([v] \underset{˙}{\sim}) \leq 1$
86		neg1rr	$⊢ - 1 \in ℝ$
87		1re	$⊢ 1 \in ℝ$
88	86 87	elicc2i	$⊢ v - F ([v] \underset{˙}{\sim}) \in [- 1, 1] \leftrightarrow (v - F ([v] \underset{˙}{\sim}) \in ℝ \land - 1 \leq v - F ([v] \underset{˙}{\sim}) \land v - F ([v] \underset{˙}{\sim}) \leq 1)$
89	67 80 85 88	syl3anbrc	$⊢ (φ \land v \in [0, 1]) \to v - F ([v] \underset{˙}{\sim}) \in [- 1, 1]$
90	58 89	elind	$⊢ (φ \land v \in [0, 1]) \to v - F ([v] \underset{˙}{\sim}) \in (ℚ \cap [- 1, 1])$
91	33 90	ffvelcdmd	$⊢ (φ \land v \in [0, 1]) \to G^{-1} (v - F ([v] \underset{˙}{\sim})) \in ℕ$
92		oveq1	$⊢ s = v \to s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) = v - G (G^{-1} (v - F ([v] \underset{˙}{\sim})))$
93	92	eleq1d	$⊢ s = v \to (s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F \leftrightarrow v - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F)$
94		f1ocnvfv2	$⊢ (G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \land v - F ([v] \underset{˙}{\sim}) \in (ℚ \cap [- 1, 1])) \to G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) = v - F ([v] \underset{˙}{\sim})$
95	5 90 94	syl2an2r	$⊢ (φ \land v \in [0, 1]) \to G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) = v - F ([v] \underset{˙}{\sim})$
96	95	oveq2d	$⊢ (φ \land v \in [0, 1]) \to v - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) = v - (v - F ([v] \underset{˙}{\sim}))$
97	78 77	nncand	$⊢ (φ \land v \in [0, 1]) \to v - (v - F ([v] \underset{˙}{\sim})) = F ([v] \underset{˙}{\sim})$
98	96 97	eqtrd	$⊢ (φ \land v \in [0, 1]) \to v - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) = F ([v] \underset{˙}{\sim})$
99		fnfvelrn	$⊢ (F Fn S \land [v] \underset{˙}{\sim} \in S) \to F ([v] \underset{˙}{\sim}) \in ran F$
100	3 47 99	syl2an2r	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \in ran F$
101	98 100	eqeltrd	$⊢ (φ \land v \in [0, 1]) \to v - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F$
102	93 61 101	elrabd	$⊢ (φ \land v \in [0, 1]) \to v \in \{s \in ℝ \| s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F\}$
103		fveq2	$⊢ n = G^{-1} (v - F ([v] \underset{˙}{\sim})) \to G (n) = G (G^{-1} (v - F ([v] \underset{˙}{\sim})))$
104	103	oveq2d	$⊢ n = G^{-1} (v - F ([v] \underset{˙}{\sim})) \to s - G (n) = s - G (G^{-1} (v - F ([v] \underset{˙}{\sim})))$
105	104	eleq1d	$⊢ n = G^{-1} (v - F ([v] \underset{˙}{\sim})) \to (s - G (n) \in ran F \leftrightarrow s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F)$
106	105	rabbidv	$⊢ n = G^{-1} (v - F ([v] \underset{˙}{\sim})) \to \{s \in ℝ \| s - G (n) \in ran F\} = \{s \in ℝ \| s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F\}$
107		reex	$⊢ ℝ \in V$
108	107	rabex	$⊢ \{s \in ℝ \| s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F\} \in V$
109	106 6 108	fvmpt	$⊢ G^{-1} (v - F ([v] \underset{˙}{\sim})) \in ℕ \to T (G^{-1} (v - F ([v] \underset{˙}{\sim}))) = \{s \in ℝ \| s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F\}$
110	91 109	syl	$⊢ (φ \land v \in [0, 1]) \to T (G^{-1} (v - F ([v] \underset{˙}{\sim}))) = \{s \in ℝ \| s - G (G^{-1} (v - F ([v] \underset{˙}{\sim}))) \in ran F\}$
111	102 110	eleqtrrd	$⊢ (φ \land v \in [0, 1]) \to v \in T (G^{-1} (v - F ([v] \underset{˙}{\sim})))$
112		fveq2	$⊢ m = G^{-1} (v - F ([v] \underset{˙}{\sim})) \to T (m) = T (G^{-1} (v - F ([v] \underset{˙}{\sim})))$
113	112	eliuni	$⊢ (G^{-1} (v - F ([v] \underset{˙}{\sim})) \in ℕ \land v \in T (G^{-1} (v - F ([v] \underset{˙}{\sim})))) \to v \in ⋃_{m \in ℕ} T (m)$
114	91 111 113	syl2anc	$⊢ (φ \land v \in [0, 1]) \to v \in ⋃_{m \in ℕ} T (m)$
115	114	ex	$⊢ φ \to (v \in [0, 1] \to v \in ⋃_{m \in ℕ} T (m))$
116	115	ssrdv	$⊢ φ \to [0, 1] \subseteq ⋃_{m \in ℕ} T (m)$
117		eliun	$⊢ x \in ⋃_{m \in ℕ} T (m) \leftrightarrow \exists m \in ℕ x \in T (m)$
118		fveq2	$⊢ n = m \to G (n) = G (m)$
119	118	oveq2d	$⊢ n = m \to s - G (n) = s - G (m)$
120	119	eleq1d	$⊢ n = m \to (s - G (n) \in ran F \leftrightarrow s - G (m) \in ran F)$
121	120	rabbidv	$⊢ n = m \to \{s \in ℝ \| s - G (n) \in ran F\} = \{s \in ℝ \| s - G (m) \in ran F\}$
122	107	rabex	$⊢ \{s \in ℝ \| s - G (m) \in ran F\} \in V$
123	121 6 122	fvmpt	$⊢ m \in ℕ \to T (m) = \{s \in ℝ \| s - G (m) \in ran F\}$
124	123	adantl	$⊢ (φ \land m \in ℕ) \to T (m) = \{s \in ℝ \| s - G (m) \in ran F\}$
125	124	eleq2d	$⊢ (φ \land m \in ℕ) \to (x \in T (m) \leftrightarrow x \in \{s \in ℝ \| s - G (m) \in ran F\})$
126	125	biimpa	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x \in \{s \in ℝ \| s - G (m) \in ran F\}$
127		oveq1	$⊢ s = x \to s - G (m) = x - G (m)$
128	127	eleq1d	$⊢ s = x \to (s - G (m) \in ran F \leftrightarrow x - G (m) \in ran F)$
129	128	elrab	$⊢ x \in \{s \in ℝ \| s - G (m) \in ran F\} \leftrightarrow (x \in ℝ \land x - G (m) \in ran F)$
130	126 129	sylib	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to (x \in ℝ \land x - G (m) \in ran F)$
131	130	simpld	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x \in ℝ$
132	86	a1i	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to - 1 \in ℝ$
133		iccssre	$⊢ (- 1 \in ℝ \land 1 \in ℝ) \to [- 1, 1] \subseteq ℝ$
134	86 87 133	mp2an	$⊢ [- 1, 1] \subseteq ℝ$
135		f1of	$⊢ G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
136	5 135	syl	$⊢ φ \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
137	136	ffvelcdmda	$⊢ (φ \land m \in ℕ) \to G (m) \in (ℚ \cap [- 1, 1])$
138	137	elin2d	$⊢ (φ \land m \in ℕ) \to G (m) \in [- 1, 1]$
139	134 138	sselid	$⊢ (φ \land m \in ℕ) \to G (m) \in ℝ$
140	139	adantr	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to G (m) \in ℝ$
141	138	adantr	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to G (m) \in [- 1, 1]$
142	86 87	elicc2i	$⊢ G (m) \in [- 1, 1] \leftrightarrow (G (m) \in ℝ \land - 1 \leq G (m) \land G (m) \leq 1)$
143	141 142	sylib	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to (G (m) \in ℝ \land - 1 \leq G (m) \land G (m) \leq 1)$
144	143	simp2d	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to - 1 \leq G (m)$
145	29	ad2antrr	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to ran F \subseteq [0, 1]$
146	130	simprd	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x - G (m) \in ran F$
147	145 146	sseldd	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x - G (m) \in [0, 1]$
148		elicc01	$⊢ x - G (m) \in [0, 1] \leftrightarrow (x - G (m) \in ℝ \land 0 \leq x - G (m) \land x - G (m) \leq 1)$
149	147 148	sylib	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to (x - G (m) \in ℝ \land 0 \leq x - G (m) \land x - G (m) \leq 1)$
150	149	simp2d	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to 0 \leq x - G (m)$
151	131 140	subge0d	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to (0 \leq x - G (m) \leftrightarrow G (m) \leq x)$
152	150 151	mpbid	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to G (m) \leq x$
153	132 140 131 144 152	letrd	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to - 1 \leq x$
154		peano2re	$⊢ G (m) \in ℝ \to G (m) + 1 \in ℝ$
155	140 154	syl	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to G (m) + 1 \in ℝ$
156		2re	$⊢ 2 \in ℝ$
157	156	a1i	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to 2 \in ℝ$
158	149	simp3d	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x - G (m) \leq 1$
159		1red	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to 1 \in ℝ$
160	131 140 159	lesubadd2d	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to (x - G (m) \leq 1 \leftrightarrow x \leq G (m) + 1)$
161	158 160	mpbid	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x \leq G (m) + 1$
162	143	simp3d	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to G (m) \leq 1$
163	140 159 159 162	leadd1dd	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to G (m) + 1 \leq 1 + 1$
164		df-2	$⊢ 2 = 1 + 1$
165	163 164	breqtrrdi	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to G (m) + 1 \leq 2$
166	131 155 157 161 165	letrd	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x \leq 2$
167	86 156	elicc2i	$⊢ x \in [- 1, 2] \leftrightarrow (x \in ℝ \land - 1 \leq x \land x \leq 2)$
168	131 153 166 167	syl3anbrc	$⊢ ((φ \land m \in ℕ) \land x \in T (m)) \to x \in [- 1, 2]$
169	168	rexlimdva2	$⊢ φ \to (\exists m \in ℕ x \in T (m) \to x \in [- 1, 2])$
170	117 169	biimtrid	$⊢ φ \to (x \in ⋃_{m \in ℕ} T (m) \to x \in [- 1, 2])$
171	170	ssrdv	$⊢ φ \to ⋃_{m \in ℕ} T (m) \subseteq [- 1, 2]$
172	29 116 171	3jca	$⊢ φ \to (ran F \subseteq [0, 1] \land [0, 1] \subseteq ⋃_{m \in ℕ} T (m) \land ⋃_{m \in ℕ} T (m) \subseteq [- 1, 2])$

Metamath Proof Explorer

Theorem vitalilem2

Proof