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	ffvelrnd	$⊢ (φ \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	ffvelrnd	$⊢ (φ \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		simpr	$⊢ (φ \land v \in [0, 1]) \to v \in [0, 1]$
80		erdm	$⊢ \underset{˙}{\sim} Er [0, 1] \to dom \underset{˙}{\sim} = [0, 1]$
81	38 80	ax-mp	$⊢ dom \underset{˙}{\sim} = [0, 1]$
82	81	eleq2i	$⊢ v \in dom \underset{˙}{\sim} \leftrightarrow v \in [0, 1]$
83		ecdmn0	$⊢ v \in dom \underset{˙}{\sim} \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset$
84	82 83	bitr3i	$⊢ v \in [0, 1] \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset$
85	79 84	sylib	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} \neq \emptyset$
86		neeq1	$⊢ z = [v] \underset{˙}{\sim} \to (z \neq \emptyset \leftrightarrow [v] \underset{˙}{\sim} \neq \emptyset)$
87		fveq2	$⊢ z = [v] \underset{˙}{\sim} \to F (z) = F ([v] \underset{˙}{\sim})$
88		id	$⊢ z = [v] \underset{˙}{\sim} \to z = [v] \underset{˙}{\sim}$
89	87 88	eleq12d	$⊢ z = [v] \underset{˙}{\sim} \to (F (z) \in z \leftrightarrow F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim})$
90	86 89	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}))$
91	4	adantr	$⊢ (φ \land v \in [0, 1]) \to \forall z \in S (z \neq \emptyset \to F (z) \in z)$
92		ovex	$⊢ [0, 1] \in V$
93		erex	$⊢ \underset{˙}{\sim} Er [0, 1] \to ([0, 1] \in V \to \underset{˙}{\sim} \in V)$
94	38 92 93	mp2	$⊢ \underset{˙}{\sim} \in V$
95	94	ecelqsi	$⊢ v \in [0, 1] \to [v] \underset{˙}{\sim} \in ([0, 1] / \underset{˙}{\sim})$
96	95 2	eleqtrrdi	$⊢ v \in [0, 1] \to [v] \underset{˙}{\sim} \in S$
97	96	adantl	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} \in S$
98	90 91 97	rspcdva	$⊢ (φ \land v \in [0, 1]) \to ([v] \underset{˙}{\sim} \neq \emptyset \to F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim})$
99	85 98	mpd	$⊢ (φ \land v \in [0, 1]) \to F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim}$
100		fvex	$⊢ F ([v] \underset{˙}{\sim}) \in V$
101		vex	$⊢ v \in V$
102	100 101	elec	$⊢ F ([v] \underset{˙}{\sim}) \in [v] \underset{˙}{\sim} \leftrightarrow v \underset{˙}{\sim} F ([v] \underset{˙}{\sim})$
103	99 102	sylib	$⊢ (φ \land v \in [0, 1]) \to v \underset{˙}{\sim} F ([v] \underset{˙}{\sim})$
104	78 103	erthi	$⊢ (φ \land v \in [0, 1]) \to [v] \underset{˙}{\sim} = [F ([v] \underset{˙}{\sim})] \underset{˙}{\sim}$
105	104	eqcomd	$⊢ (φ \land v \in [0, 1]) \to [F ([v] \underset{˙}{\sim})] \underset{˙}{\sim} = [v] \underset{˙}{\sim}$
106	105	fveq2d	$⊢ (φ \land v \in [0, 1]) \to F ([F ([v] \underset{˙}{\sim})] \underset{˙}{\sim}) = F ([v] \underset{˙}{\sim})$
107	2 77 106	ectocld	$⊢ (φ \land w \in S) \to F ([F (w)] \underset{˙}{\sim}) = F (w)$
108	107	ralrimiva	$⊢ φ \to \forall w \in S F ([F (w)] \underset{˙}{\sim}) = F (w)$
109		eceq1	$⊢ z = F (w) \to [z] \underset{˙}{\sim} = [F (w)] \underset{˙}{\sim}$
110	109	fveq2d	$⊢ z = F (w) \to F ([z] \underset{˙}{\sim}) = F ([F (w)] \underset{˙}{\sim})$
111		id	$⊢ z = F (w) \to z = F (w)$
112	110 111	eqeq12d	$⊢ z = F (w) \to (F ([z] \underset{˙}{\sim}) = z \leftrightarrow F ([F (w)] \underset{˙}{\sim}) = F (w))$
113	112	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))$
114	3 113	syl	$⊢ φ \to (\forall z \in ran F F ([z] \underset{˙}{\sim}) = z \leftrightarrow \forall w \in S F ([F (w)] \underset{˙}{\sim}) = F (w))$
115	108 114	mpbird	$⊢ φ \to \forall z \in ran F F ([z] \underset{˙}{\sim}) = z$
116	115	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$
117	73 116 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)$
118		eceq1	$⊢ z = w - G (k) \to [z] \underset{˙}{\sim} = [(w - G (k))] \underset{˙}{\sim}$
119	118	fveq2d	$⊢ z = w - G (k) \to F ([z] \underset{˙}{\sim}) = F ([(w - G (k))] \underset{˙}{\sim})$
120		id	$⊢ z = w - G (k) \to z = w - G (k)$
121	119 120	eqeq12d	$⊢ z = w - G (k) \to (F ([z] \underset{˙}{\sim}) = z \leftrightarrow F ([(w - G (k))] \underset{˙}{\sim}) = w - G (k))$
122	121 116 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)$
123	69 117 122	3eqtr3d	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to w - G (m) = w - G (k)$
124	24 33 37 123	subcand	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to G (m) = G (k)$
125	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]$
126		f1of1	$⊢ G : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to G : ℕ \underset{1-1}{⟶} ℚ \cap [- 1, 1]$
127	125 126	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]$
128		f1fveq	$⊢ (G : ℕ \underset{1-1}{⟶} ℚ \cap [- 1, 1] \land (m \in ℕ \land k \in ℕ)) \to (G (m) = G (k) \leftrightarrow m = k)$
129	127 9 34 128	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)$
130	124 129	mpbid	$⊢ (φ \land ((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k)))) \to m = k$
131	130	ex	$⊢ φ \to (((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k))) \to m = k)$
132	131	alrimivv	$⊢ φ \to \forall m \forall k (((m \in ℕ \land w \in T (m)) \land (k \in ℕ \land w \in T (k))) \to m = k)$
133		eleq1w	$⊢ m = k \to (m \in ℕ \leftrightarrow k \in ℕ)$
134		fveq2	$⊢ m = k \to T (m) = T (k)$
135	134	eleq2d	$⊢ m = k \to (w \in T (m) \leftrightarrow w \in T (k))$
136	133 135	anbi12d	$⊢ m = k \to ((m \in ℕ \land w \in T (m)) \leftrightarrow (k \in ℕ \land w \in T (k)))$
137	136	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)$
138	132 137	sylibr	$⊢ φ \to \exists^{*} m (m \in ℕ \land w \in T (m))$
139	138	alrimiv	$⊢ φ \to \forall w \exists^{*} m (m \in ℕ \land w \in T (m))$
140		dfdisj2	$⊢ \underset{m \in ℕ}{Disj} T (m) \leftrightarrow \forall w \exists^{*} m (m \in ℕ \land w \in T (m))$
141	139 140	sylibr	$⊢ φ \to \underset{m \in ℕ}{Disj} T (m)$

Metamath Proof Explorer

Theorem vitalilem3

Proof