dyadmbl

Description: Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015)

	Ref	Expression
Hypotheses	dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
	dyadmbl.2	$⊢ G = \{z \in A \| \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)\}$
	dyadmbl.3	$⊢ φ \to A \subseteq ran F$
Assertion	dyadmbl	$⊢ φ \to ⋃ [.] [A] \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2		dyadmbl.2	$⊢ G = \{z \in A \| \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)\}$
3		dyadmbl.3	$⊢ φ \to A \subseteq ran F$
4	1 2 3	dyadmbllem	$⊢ φ \to ⋃ [.] [A] = ⋃ [.] [G]$
5		isfinite	$⊢ G \in Fin \leftrightarrow G ≺ ω$
6		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
7		ffun	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*} \to Fun [.]$
8		funiunfv	$⊢ Fun [.] \to ⋃_{n \in G} [.] (n) = ⋃ [.] [G]$
9	6 7 8	mp2b	$⊢ ⋃_{n \in G} [.] (n) = ⋃ [.] [G]$
10		simpr	$⊢ (φ \land G \in Fin) \to G \in Fin$
11	2	ssrab3	$⊢ G \subseteq A$
12	11 3	sstrid	$⊢ φ \to G \subseteq ran F$
13	1	dyadf	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
14		frn	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to ran F \subseteq \leq \cap ℝ^{2}$
15	13 14	ax-mp	$⊢ ran F \subseteq \leq \cap ℝ^{2}$
16		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
17	15 16	sstri	$⊢ ran F \subseteq ℝ^{2}$
18	12 17	sstrdi	$⊢ φ \to G \subseteq ℝ^{2}$
19	18	adantr	$⊢ (φ \land G \in Fin) \to G \subseteq ℝ^{2}$
20	19	sselda	$⊢ ((φ \land G \in Fin) \land n \in G) \to n \in ℝ^{2}$
21		1st2nd2	$⊢ n \in ℝ^{2} \to n = ⟨1^{st} (n), 2^{nd} (n)⟩$
22	20 21	syl	$⊢ ((φ \land G \in Fin) \land n \in G) \to n = ⟨1^{st} (n), 2^{nd} (n)⟩$
23	22	fveq2d	$⊢ ((φ \land G \in Fin) \land n \in G) \to [.] (n) = [.] (⟨1^{st} (n), 2^{nd} (n)⟩)$
24		df-ov	$⊢ [1^{st} (n), 2^{nd} (n)] = [.] (⟨1^{st} (n), 2^{nd} (n)⟩)$
25	23 24	eqtr4di	$⊢ ((φ \land G \in Fin) \land n \in G) \to [.] (n) = [1^{st} (n), 2^{nd} (n)]$
26		xp1st	$⊢ n \in ℝ^{2} \to 1^{st} (n) \in ℝ$
27	20 26	syl	$⊢ ((φ \land G \in Fin) \land n \in G) \to 1^{st} (n) \in ℝ$
28		xp2nd	$⊢ n \in ℝ^{2} \to 2^{nd} (n) \in ℝ$
29	20 28	syl	$⊢ ((φ \land G \in Fin) \land n \in G) \to 2^{nd} (n) \in ℝ$
30		iccmbl	$⊢ (1^{st} (n) \in ℝ \land 2^{nd} (n) \in ℝ) \to [1^{st} (n), 2^{nd} (n)] \in dom vol$
31	27 29 30	syl2anc	$⊢ ((φ \land G \in Fin) \land n \in G) \to [1^{st} (n), 2^{nd} (n)] \in dom vol$
32	25 31	eqeltrd	$⊢ ((φ \land G \in Fin) \land n \in G) \to [.] (n) \in dom vol$
33	32	ralrimiva	$⊢ (φ \land G \in Fin) \to \forall n \in G [.] (n) \in dom vol$
34		finiunmbl	$⊢ (G \in Fin \land \forall n \in G [.] (n) \in dom vol) \to ⋃_{n \in G} [.] (n) \in dom vol$
35	10 33 34	syl2anc	$⊢ (φ \land G \in Fin) \to ⋃_{n \in G} [.] (n) \in dom vol$
36	9 35	eqeltrrid	$⊢ (φ \land G \in Fin) \to ⋃ [.] [G] \in dom vol$
37	5 36	sylan2br	$⊢ (φ \land G ≺ ω) \to ⋃ [.] [G] \in dom vol$
38		rnco2	$⊢ ran ([.] \circ f) = [.] [ran f]$
39		f1ofo	$⊢ f : ℕ \underset{1-1 onto}{⟶} G \to f : ℕ \underset{onto}{⟶} G$
40	39	adantl	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to f : ℕ \underset{onto}{⟶} G$
41		forn	$⊢ f : ℕ \underset{onto}{⟶} G \to ran f = G$
42	40 41	syl	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to ran f = G$
43	42	imaeq2d	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to [.] [ran f] = [.] [G]$
44	38 43	syl5eq	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to ran ([.] \circ f) = [.] [G]$
45	44	unieqd	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to ⋃ ran ([.] \circ f) = ⋃ [.] [G]$
46		f1of	$⊢ f : ℕ \underset{1-1 onto}{⟶} G \to f : ℕ ⟶ G$
47	12 15	sstrdi	$⊢ φ \to G \subseteq \leq \cap ℝ^{2}$
48		fss	$⊢ (f : ℕ ⟶ G \land G \subseteq \leq \cap ℝ^{2}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
49	46 47 48	syl2anr	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
50		fss	$⊢ (f : ℕ ⟶ G \land G \subseteq ran F) \to f : ℕ ⟶ ran F$
51	46 12 50	syl2anr	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to f : ℕ ⟶ ran F$
52		simpl	$⊢ (a \in ℕ \land b \in ℕ) \to a \in ℕ$
53		ffvelrn	$⊢ (f : ℕ ⟶ ran F \land a \in ℕ) \to f (a) \in ran F$
54	51 52 53	syl2an	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to f (a) \in ran F$
55		simpr	$⊢ (a \in ℕ \land b \in ℕ) \to b \in ℕ$
56		ffvelrn	$⊢ (f : ℕ ⟶ ran F \land b \in ℕ) \to f (b) \in ran F$
57	51 55 56	syl2an	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to f (b) \in ran F$
58	1	dyaddisj	$⊢ (f (a) \in ran F \land f (b) \in ran F) \to ([.] (f (a)) \subseteq [.] (f (b)) \lor [.] (f (b)) \subseteq [.] (f (a)) \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset)$
59	54 57 58	syl2anc	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to ([.] (f (a)) \subseteq [.] (f (b)) \lor [.] (f (b)) \subseteq [.] (f (a)) \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset)$
60		fveq2	$⊢ w = f (b) \to [.] (w) = [.] (f (b))$
61	60	sseq2d	$⊢ w = f (b) \to ([.] (f (a)) \subseteq [.] (w) \leftrightarrow [.] (f (a)) \subseteq [.] (f (b)))$
62		eqeq2	$⊢ w = f (b) \to (f (a) = w \leftrightarrow f (a) = f (b))$
63	61 62	imbi12d	$⊢ w = f (b) \to (([.] (f (a)) \subseteq [.] (w) \to f (a) = w) \leftrightarrow ([.] (f (a)) \subseteq [.] (f (b)) \to f (a) = f (b)))$
64	46	adantl	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to f : ℕ ⟶ G$
65		ffvelrn	$⊢ (f : ℕ ⟶ G \land a \in ℕ) \to f (a) \in G$
66	64 52 65	syl2an	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to f (a) \in G$
67		fveq2	$⊢ z = f (a) \to [.] (z) = [.] (f (a))$
68	67	sseq1d	$⊢ z = f (a) \to ([.] (z) \subseteq [.] (w) \leftrightarrow [.] (f (a)) \subseteq [.] (w))$
69		eqeq1	$⊢ z = f (a) \to (z = w \leftrightarrow f (a) = w)$
70	68 69	imbi12d	$⊢ z = f (a) \to (([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow ([.] (f (a)) \subseteq [.] (w) \to f (a) = w))$
71	70	ralbidv	$⊢ z = f (a) \to (\forall w \in A ([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow \forall w \in A ([.] (f (a)) \subseteq [.] (w) \to f (a) = w))$
72	71 2	elrab2	$⊢ f (a) \in G \leftrightarrow (f (a) \in A \land \forall w \in A ([.] (f (a)) \subseteq [.] (w) \to f (a) = w))$
73	72	simprbi	$⊢ f (a) \in G \to \forall w \in A ([.] (f (a)) \subseteq [.] (w) \to f (a) = w)$
74	66 73	syl	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to \forall w \in A ([.] (f (a)) \subseteq [.] (w) \to f (a) = w)$
75		ffvelrn	$⊢ (f : ℕ ⟶ G \land b \in ℕ) \to f (b) \in G$
76	64 55 75	syl2an	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to f (b) \in G$
77	11 76	sseldi	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to f (b) \in A$
78	63 74 77	rspcdva	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to ([.] (f (a)) \subseteq [.] (f (b)) \to f (a) = f (b))$
79		f1of1	$⊢ f : ℕ \underset{1-1 onto}{⟶} G \to f : ℕ \underset{1-1}{⟶} G$
80	79	adantl	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to f : ℕ \underset{1-1}{⟶} G$
81		f1fveq	$⊢ (f : ℕ \underset{1-1}{⟶} G \land (a \in ℕ \land b \in ℕ)) \to (f (a) = f (b) \leftrightarrow a = b)$
82	80 81	sylan	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to (f (a) = f (b) \leftrightarrow a = b)$
83		orc	$⊢ a = b \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset)$
84	82 83	syl6bi	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to (f (a) = f (b) \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset))$
85	78 84	syld	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to ([.] (f (a)) \subseteq [.] (f (b)) \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset))$
86		fveq2	$⊢ w = f (a) \to [.] (w) = [.] (f (a))$
87	86	sseq2d	$⊢ w = f (a) \to ([.] (f (b)) \subseteq [.] (w) \leftrightarrow [.] (f (b)) \subseteq [.] (f (a)))$
88		eqeq2	$⊢ w = f (a) \to (f (b) = w \leftrightarrow f (b) = f (a))$
89		eqcom	$⊢ f (b) = f (a) \leftrightarrow f (a) = f (b)$
90	88 89	bitrdi	$⊢ w = f (a) \to (f (b) = w \leftrightarrow f (a) = f (b))$
91	87 90	imbi12d	$⊢ w = f (a) \to (([.] (f (b)) \subseteq [.] (w) \to f (b) = w) \leftrightarrow ([.] (f (b)) \subseteq [.] (f (a)) \to f (a) = f (b)))$
92		fveq2	$⊢ z = f (b) \to [.] (z) = [.] (f (b))$
93	92	sseq1d	$⊢ z = f (b) \to ([.] (z) \subseteq [.] (w) \leftrightarrow [.] (f (b)) \subseteq [.] (w))$
94		eqeq1	$⊢ z = f (b) \to (z = w \leftrightarrow f (b) = w)$
95	93 94	imbi12d	$⊢ z = f (b) \to (([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow ([.] (f (b)) \subseteq [.] (w) \to f (b) = w))$
96	95	ralbidv	$⊢ z = f (b) \to (\forall w \in A ([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow \forall w \in A ([.] (f (b)) \subseteq [.] (w) \to f (b) = w))$
97	96 2	elrab2	$⊢ f (b) \in G \leftrightarrow (f (b) \in A \land \forall w \in A ([.] (f (b)) \subseteq [.] (w) \to f (b) = w))$
98	97	simprbi	$⊢ f (b) \in G \to \forall w \in A ([.] (f (b)) \subseteq [.] (w) \to f (b) = w)$
99	76 98	syl	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to \forall w \in A ([.] (f (b)) \subseteq [.] (w) \to f (b) = w)$
100	11 66	sseldi	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to f (a) \in A$
101	91 99 100	rspcdva	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to ([.] (f (b)) \subseteq [.] (f (a)) \to f (a) = f (b))$
102	101 84	syld	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to ([.] (f (b)) \subseteq [.] (f (a)) \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset))$
103		olc	$⊢ (.) (f (a)) \cap (.) (f (b)) = \emptyset \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset)$
104	103	a1i	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to ((.) (f (a)) \cap (.) (f (b)) = \emptyset \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset))$
105	85 102 104	3jaod	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to (([.] (f (a)) \subseteq [.] (f (b)) \lor [.] (f (b)) \subseteq [.] (f (a)) \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset) \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset))$
106	59 105	mpd	$⊢ ((φ \land f : ℕ \underset{1-1 onto}{⟶} G) \land (a \in ℕ \land b \in ℕ)) \to (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset)$
107	106	ralrimivva	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to \forall a \in ℕ \forall b \in ℕ (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset)$
108		2fveq3	$⊢ a = b \to (.) (f (a)) = (.) (f (b))$
109	108	disjor	$⊢ \underset{a \in ℕ}{Disj} (.) (f (a)) \leftrightarrow \forall a \in ℕ \forall b \in ℕ (a = b \lor (.) (f (a)) \cap (.) (f (b)) = \emptyset)$
110	107 109	sylibr	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to \underset{a \in ℕ}{Disj} (.) (f (a))$
111		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
112	49 110 111	uniiccmbl	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to ⋃ ran ([.] \circ f) \in dom vol$
113	45 112	eqeltrrd	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} G) \to ⋃ [.] [G] \in dom vol$
114	113	ex	$⊢ φ \to (f : ℕ \underset{1-1 onto}{⟶} G \to ⋃ [.] [G] \in dom vol)$
115	114	exlimdv	$⊢ φ \to (\exists f f : ℕ \underset{1-1 onto}{⟶} G \to ⋃ [.] [G] \in dom vol)$
116		nnenom	$⊢ ℕ \approx ω$
117		ensym	$⊢ G \approx ω \to ω \approx G$
118		entr	$⊢ (ℕ \approx ω \land ω \approx G) \to ℕ \approx G$
119	116 117 118	sylancr	$⊢ G \approx ω \to ℕ \approx G$
120		bren	$⊢ ℕ \approx G \leftrightarrow \exists f f : ℕ \underset{1-1 onto}{⟶} G$
121	119 120	sylib	$⊢ G \approx ω \to \exists f f : ℕ \underset{1-1 onto}{⟶} G$
122	115 121	impel	$⊢ (φ \land G \approx ω) \to ⋃ [.] [G] \in dom vol$
123		reex	$⊢ ℝ \in V$
124	123 123	xpex	$⊢ ℝ^{2} \in V$
125	124	inex2	$⊢ \leq \cap ℝ^{2} \in V$
126	125 15	ssexi	$⊢ ran F \in V$
127		ssdomg	$⊢ ran F \in V \to (G \subseteq ran F \to G ≼ ran F)$
128	126 12 127	mpsyl	$⊢ φ \to G ≼ ran F$
129		omelon	$⊢ ω \in On$
130		znnen	$⊢ ℤ \approx ℕ$
131	130 116	entri	$⊢ ℤ \approx ω$
132		nn0ennn	$⊢ ℕ_{0} \approx ℕ$
133	132 116	entri	$⊢ ℕ_{0} \approx ω$
134		xpen	$⊢ (ℤ \approx ω \land ℕ_{0} \approx ω) \to (ℤ \times ℕ_{0}) \approx (ω \times ω)$
135	131 133 134	mp2an	$⊢ (ℤ \times ℕ_{0}) \approx (ω \times ω)$
136		xpomen	$⊢ (ω \times ω) \approx ω$
137	135 136	entri	$⊢ (ℤ \times ℕ_{0}) \approx ω$
138	137	ensymi	$⊢ ω \approx (ℤ \times ℕ_{0})$
139		isnumi	$⊢ (ω \in On \land ω \approx (ℤ \times ℕ_{0})) \to ℤ \times ℕ_{0} \in dom card$
140	129 138 139	mp2an	$⊢ ℤ \times ℕ_{0} \in dom card$
141		ffn	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to F Fn (ℤ \times ℕ_{0})$
142	13 141	ax-mp	$⊢ F Fn (ℤ \times ℕ_{0})$
143		dffn4	$⊢ F Fn (ℤ \times ℕ_{0}) \leftrightarrow F : ℤ \times ℕ_{0} \underset{onto}{⟶} ran F$
144	142 143	mpbi	$⊢ F : ℤ \times ℕ_{0} \underset{onto}{⟶} ran F$
145		fodomnum	$⊢ ℤ \times ℕ_{0} \in dom card \to (F : ℤ \times ℕ_{0} \underset{onto}{⟶} ran F \to ran F ≼ (ℤ \times ℕ_{0}))$
146	140 144 145	mp2	$⊢ ran F ≼ (ℤ \times ℕ_{0})$
147		domentr	$⊢ (ran F ≼ (ℤ \times ℕ_{0}) \land (ℤ \times ℕ_{0}) \approx ω) \to ran F ≼ ω$
148	146 137 147	mp2an	$⊢ ran F ≼ ω$
149		domtr	$⊢ (G ≼ ran F \land ran F ≼ ω) \to G ≼ ω$
150	128 148 149	sylancl	$⊢ φ \to G ≼ ω$
151		brdom2	$⊢ G ≼ ω \leftrightarrow (G ≺ ω \lor G \approx ω)$
152	150 151	sylib	$⊢ φ \to (G ≺ ω \lor G \approx ω)$
153	37 122 152	mpjaodan	$⊢ φ \to ⋃ [.] [G] \in dom vol$
154	4 153	eqeltrd	$⊢ φ \to ⋃ [.] [A] \in dom vol$

Metamath Proof Explorer

Theorem dyadmbl

Proof