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