vitalilem3

	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	vitalilem3	$⊢ φ \to \underset{m \in ℕ}{Disj} T (m)$

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		simprlr	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w \in T (m)$
9		simprll	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to m \in ℕ$
10		fveq2	$⊢ n = m \to G (n) = G (m)$
11	10	oveq2d	$⊢ n = m \to s - G (n) = s - G (m)$
12	11	eleq1d	$⊢ n = m \to (s - G (n) \in ran F \leftrightarrow s - G (m) \in ran F)$
13	12	rabbidv	$⊢ n = m \to \{s \in ℝ \| s - G (n) \in ran F\} = \{s \in ℝ \| s - G (m) \in ran F\}$
14		reex	$⊢ ℝ \in V$
15	14	rabex	$⊢ \{s \in ℝ \| s - G (m) \in ran F\} \in V$
16	13 6 15	fvmpt	$⊢ m \in ℕ \to T (m) = \{s \in ℝ \| s - G (m) \in ran F\}$
17	9 16	syl	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to T (m) = \{s \in ℝ \| s - G (m) \in ran F\}$
18	8 17	eleqtrd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w \in \{s \in ℝ \| s - G (m) \in ran F\}$
19		oveq1	$⊢ s = w \to s - G (m) = w - G (m)$
20	19	eleq1d	$⊢ s = w \to (s - G (m) \in ran F \leftrightarrow w - G (m) \in ran F)$
21	20	elrab	$⊢ w \in \{s \in ℝ \| s - G (m) \in ran F\} \leftrightarrow (w \in ℝ \land w - G (m) \in ran F)$
22	18 21	sylib	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to (w \in ℝ \land w - G (m) \in ran F)$
23	22	simpld	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w \in ℝ$
24	23	recnd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w \in ℂ$
25		f1of	$⊢ G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
26	5 25	syl	$⊢ φ \to G : ℕ ⟶ ℚ \cap [- 1, 1]$
27		inss1	$⊢ ℚ \cap [- 1, 1] \subseteq ℚ$
28		fss	$⊢ (G : ℕ ⟶ ℚ \cap [- 1, 1] \land ℚ \cap [- 1, 1] \subseteq ℚ) \to G : ℕ ⟶ ℚ$
29	26 27 28	sylancl	$⊢ φ \to G : ℕ ⟶ ℚ$
30	29	adantr	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G : ℕ ⟶ ℚ$
31	30 9	ffvelcdmd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G (m) \in ℚ$
32		qcn	$⊢ G (m) \in ℚ \to G (m) \in ℂ$
33	31 32	syl	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G (m) \in ℂ$
34		simprrl	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to k \in ℕ$
35	30 34	ffvelcdmd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G (k) \in ℚ$
36		qcn	$⊢ G (k) \in ℚ \to G (k) \in ℂ$
37	35 36	syl	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G (k) \in ℂ$
38	1	vitalilem1	$⊢ \underset{˙}{\sim} Er [0, 1]$
39	38	a1i	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to \underset{˙}{\sim} Er [0, 1]$
40	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])$
41	40	simp1d	$⊢ φ \to ran F \subseteq [0, 1]$
42	41	adantr	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to ran F \subseteq [0, 1]$
43	22	simprd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (m) \in ran F$
44	42 43	sseldd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (m) \in [0, 1]$
45		simprrr	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w \in T (k)$
46		fveq2	$⊢ n = k \to G (n) = G (k)$
47	46	oveq2d	$⊢ n = k \to s - G (n) = s - G (k)$
48	47	eleq1d	$⊢ n = k \to (s - G (n) \in ran F \leftrightarrow s - G (k) \in ran F)$
49	48	rabbidv	$⊢ n = k \to \{s \in ℝ \| s - G (n) \in ran F\} = \{s \in ℝ \| s - G (k) \in ran F\}$
50	14	rabex	$⊢ \{s \in ℝ \| s - G (k) \in ran F\} \in V$
51	49 6 50	fvmpt	$⊢ k \in ℕ \to T (k) = \{s \in ℝ \| s - G (k) \in ran F\}$
52	34 51	syl	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to T (k) = \{s \in ℝ \| s - G (k) \in ran F\}$
53	45 52	eleqtrd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w \in \{s \in ℝ \| s - G (k) \in ran F\}$
54		oveq1	$⊢ s = w \to s - G (k) = w - G (k)$
55	54	eleq1d	$⊢ s = w \to (s - G (k) \in ran F \leftrightarrow w - G (k) \in ran F)$
56	55	elrab	$⊢ w \in \{s \in ℝ \| s - G (k) \in ran F\} \leftrightarrow (w \in ℝ \land w - G (k) \in ran F)$
57	53 56	sylib	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to (w \in ℝ \land w - G (k) \in ran F)$
58	57	simprd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (k) \in ran F$
59	42 58	sseldd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (k) \in [0, 1]$
60	24 33 37	nnncan1d	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (m) - (w - G (k)) = G (k) - G (m)$
61		qsubcl	$⊢ (G (k) \in ℚ \land G (m) \in ℚ) \to G (k) - G (m) \in ℚ$
62	35 31 61	syl2anc	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G (k) - G (m) \in ℚ$
63	60 62	eqeltrd	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (m) - (w - G (k)) \in ℚ$
64		oveq12	$⊢ (x = w - G (m) \land y = w - G (k)) \to x - y = w - G (m) - (w - G (k))$
65	64	eleq1d	$⊢ (x = w - G (m) \land y = w - G (k)) \to (x - y \in ℚ \leftrightarrow w - G (m) - (w - G (k)) \in ℚ)$
66	65 1	brab2a	$⊢ (w - G (m)) \underset{˙}{\sim} (w - G (k)) \leftrightarrow ((w - G (m) \in [0, 1] \land w - G (k) \in [0, 1]) \land w - G (m) - (w - G (k)) \in ℚ)$
67	44 59 63 66	syl21anbrc	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to (w - G (m)) \underset{˙}{\sim} (w - G (k))$
68	39 67	erthi	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to [(w - G (m))] \underset{˙}{\sim} = [(w - G (k))] \underset{˙}{\sim}$
69	68	fveq2d	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to F ([(w - G (m))] \underset{˙}{\sim}) = F ([(w - G (k))] \underset{˙}{\sim})$
70		eceq1	$⊢ z = w - G (m) \to [z] \underset{˙}{\sim} = [(w - G (m))] \underset{˙}{\sim}$
71	70	fveq2d	$⊢ z = w - G (m) \to F ([z] \underset{˙}{\sim}) = F ([(w - G (m))] \underset{˙}{\sim})$
72		id	$⊢ z = w - G (m) \to z = w - G (m)$
73	71 72	eqeq12d	$⊢ z = w - G (m) \to (F ([z] \underset{˙}{\sim}) = z \leftrightarrow F ([(w - G (m))] \underset{˙}{\sim}) = w - G (m))$
74		fveq2	$⊢ [v] \underset{˙}{\sim} = w \to F ([v] \underset{˙}{\sim}) = F (w)$
75	74	eceq1d	$⊢ [v] \underset{˙}{\sim} = w \to [F ([v] \underset{˙}{\sim})] \underset{˙}{\sim} = [F (w)] \underset{˙}{\sim}$
76	75	fveq2d	$⊢ [v] \underset{˙}{\sim} = w \to F ([F ([v] \underset{˙}{\sim})] \underset{˙}{\sim}) = F ([F (w)] \underset{˙}{\sim})$
77	76 74	eqeq12d	$⊢ [v] \underset{˙}{\sim} = w \to (F ([F ([v] \underset{˙}{\sim})] \underset{˙}{\sim}) = F ([v] \underset{˙}{\sim}) \leftrightarrow F ([F (w)] \underset{˙}{\sim}) = F (w))$
78	38	a1i	$⊢ (φ \land v \in [0, 1]) \to \underset{˙}{\sim} Er [0, 1]$
79		erdm	$⊢ \underset{˙}{\sim} Er [0, 1] \to dom \underset{˙}{\sim} = [0, 1]$
80	38 79	ax-mp	$⊢ dom \underset{˙}{\sim} = [0, 1]$
81	80	eleq2i	$⊢ v \in dom \underset{˙}{\sim} \leftrightarrow v \in [0, 1]$
82		ecdmn0	$⊢ v \in dom \underset{˙}{\sim} \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset$
83	81 82	bitr3i	$⊢ v \in [0, 1] \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset$
84	83	bilani	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} \neq \emptyset$
85		neeq1	$⊢ z = [v] \underset{˙}{\sim} \to (z \neq \emptyset \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset)$
86		fveq2	$⊢ z = [v] \underset{˙}{\sim} \to F (z) = F ([v] \underset{˙}{\sim})$
87		id	$⊢ z = [v] \underset{˙}{\sim} \to z = [v] \underset{˙}{\sim}$
88	86 87	eleq12d	$⊢ z = [v] \underset{˙}{\sim} \to (F (z) \in z \leftrightarrow F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim})$
89	85 88	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}))$
90	4	adantr	$⊢ (φ \land v \in [0, 1]) \to \forall z \in S (z \neq \emptyset \to F (z) \in z)$
91		ovex	$⊢ [0, 1] \in V$
92		erex	$⊢ \underset{˙}{\sim} Er [0, 1] \to ([0, 1] \in V \to \underset{˙}{\sim} \in V)$
93	38 91 92	mp2	$⊢ \underset{˙}{\sim} \in V$
94	93	ecelqsi	$⊢ v \in [0, 1] \to [v] \underset{˙}{\sim} \in ([0, 1] / \underset{˙}{\sim})$
95	94 2	eleqtrrdi	$⊢ v \in [0, 1] \to [v] \underset{˙}{\sim} \in S$
96	95	adantl	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} \in S$
97	89 90 96	rspcdva	$⊢ (φ \land v \in [0, 1]) \to ([v] \underset{˙}{\sim} \neq \emptyset \to F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim})$
98	84 97	mpd	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim}$
99		fvex	$⊢ F ([v] \underset{˙}{\sim}) \in V$
100		vex	$⊢ v \in V$
101	99 100	elec	$⊢ F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim} \leftrightarrow v \underset{˙}{\sim} F ([v] \underset{˙}{\sim})$
102	98 101	sylib	$⊢ (φ \land v \in [0, 1]) \to v \underset{˙}{\sim} F ([v] \underset{˙}{\sim})$
103	78 102	erthi	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} = [F ([v] \underset{˙}{\sim})] \underset{˙}{\sim}$
104	103	eqcomd	$⊢ (φ \land v \in [0, 1]) \to [F ([v] \underset{˙}{\sim})] \underset{˙}{\sim} = [v] \underset{˙}{\sim}$
105	104	fveq2d	$⊢ (φ \land v \in [0, 1]) \to F ([F ([v] \underset{˙}{\sim})] \underset{˙}{\sim}) = F ([v] \underset{˙}{\sim})$
106	2 77 105	ectocld	$⊢ (φ \land w \in S) \to F ([F (w)] \underset{˙}{\sim}) = F (w)$
107	106	ralrimiva	$⊢ φ \to \forall w \in S F ([F (w)] \underset{˙}{\sim}) = F (w)$
108		eceq1	$⊢ z = F (w) \to [z] \underset{˙}{\sim} = [F (w)] \underset{˙}{\sim}$
109	108	fveq2d	$⊢ z = F (w) \to F ([z] \underset{˙}{\sim}) = F ([F (w)] \underset{˙}{\sim})$
110		id	$⊢ z = F (w) \to z = F (w)$
111	109 110	eqeq12d	$⊢ z = F (w) \to (F ([z] \underset{˙}{\sim}) = z \leftrightarrow F ([F (w)] \underset{˙}{\sim}) = F (w))$
112	111	ralrn	$⊢ F Fn S \to (\forall z \in ran F F ([z] \underset{˙}{\sim}) = z \leftrightarrow \forall w \in S F ([F (w)] \underset{˙}{\sim}) = F (w))$
113	3 112	syl	$⊢ φ \to (\forall z \in ran F F ([z] \underset{˙}{\sim}) = z \leftrightarrow \forall w \in S F ([F (w)] \underset{˙}{\sim}) = F (w))$
114	107 113	mpbird	$⊢ φ \to \forall z \in ran F F ([z] \underset{˙}{\sim}) = z$
115	114	adantr	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to \forall z \in ran F F ([z] \underset{˙}{\sim}) = z$
116	73 115 43	rspcdva	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to F ([(w - G (m))] \underset{˙}{\sim}) = w - G (m)$
117		eceq1	$⊢ z = w - G (k) \to [z] \underset{˙}{\sim} = [(w - G (k))] \underset{˙}{\sim}$
118	117	fveq2d	$⊢ z = w - G (k) \to F ([z] \underset{˙}{\sim}) = F ([(w - G (k))] \underset{˙}{\sim})$
119		id	$⊢ z = w - G (k) \to z = w - G (k)$
120	118 119	eqeq12d	$⊢ z = w - G (k) \to (F ([z] \underset{˙}{\sim}) = z \leftrightarrow F ([(w - G (k))] \underset{˙}{\sim}) = w - G (k))$
121	120 115 58	rspcdva	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to F ([(w - G (k))] \underset{˙}{\sim}) = w - G (k)$
122	69 116 121	3eqtr3d	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (m) = w - G (k)$
123	24 33 37 122	subcand	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G (m) = G (k)$
124	5	adantr	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
125		f1of1	$⊢ G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to G : ℕ \underset{1-1}{⟶} ℚ \cap [- 1, 1]$
126	124 125	syl	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G : ℕ \underset{1-1}{⟶} ℚ \cap [- 1, 1]$
127		f1fveq	$⊢ (G : ℕ \underset{1-1}{⟶} ℚ \cap [- 1, 1] \land (m \in ℕ \land k \in ℕ)) \to (G (m) = G (k) \leftrightarrow m = k)$
128	126 9 34 127	syl12anc	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to (G (m) = G (k) \leftrightarrow m = k)$
129	123 128	mpbid	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to m = k$
130	129	ex	$⊢ φ \to (((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k))) \to m = k)$
131	130	alrimivv	$⊢ φ \to \forall m \forall k (((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k))) \to m = k)$
132		eleq1w	$⊢ m = k \to (m \in ℕ \leftrightarrow k \in ℕ)$
133		fveq2	$⊢ m = k \to T (m) = T (k)$
134	133	eleq2d	$⊢ m = k \to (w \in T (m) \leftrightarrow w \in T (k))$
135	132 134	anbi12d	$⊢ m = k \to ((m \in ℕ \land w \in T (m)) \leftrightarrow (k \in ℕ \land w \in T (k)))$
136	135	mo4	$⊢ \exists^{*} m (m \in ℕ \land w \in T (m)) \leftrightarrow \forall m \forall k (((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k))) \to m = k)$
137	131 136	sylibr	$⊢ φ \to \exists^{*} m (m \in ℕ \land w \in T (m))$
138	137	alrimiv	$⊢ φ \to \forall w \exists^{*} m (m \in ℕ \land w \in T (m))$
139		dfdisj2	$⊢ \underset{m \in ℕ}{Disj} T (m) \leftrightarrow \forall w \exists^{*} m (m \in ℕ \land w \in T (m))$
140	138 139	sylibr	$⊢ φ \to \underset{m \in ℕ}{Disj} T (m)$

Metamath Proof Explorer

Theorem vitalilem3

Proof