dya2iocct

Description: The dyadic rectangle set is countable. (Contributed by Thierry Arnoux, 18-Sep-2017) (Revised by Thierry Arnoux, 11-Oct-2017)

Step	Hyp	Ref	Expression
1		sxbrsiga.0	$⊢ J = topGen (ran (.))$
2		dya2ioc.1	$⊢ I = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
3		dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
4		znnen	$⊢ ℤ \approx ℕ$
5		nnct	$⊢ ℕ ≼ ω$
6		endomtr	$⊢ (ℤ \approx ℕ \land ℕ ≼ ω) \to ℤ ≼ ω$
7	4 5 6	mp2an	$⊢ ℤ ≼ ω$
8		ovex	$⊢ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in V$
9	8	rgen2w	$⊢ \forall x \in ℤ \forall n \in ℤ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in V$
10	9	mpocti	$⊢ (ℤ ≼ ω \land ℤ ≼ ω) \to (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) ≼ ω$
11	7 7 10	mp2an	$⊢ (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) ≼ ω$
12	2 11	eqbrtri	$⊢ I ≼ ω$
13		rnct	$⊢ I ≼ ω \to ran I ≼ ω$
14	12 13	ax-mp	$⊢ ran I ≼ ω$
15		vex	$⊢ u \in V$
16		vex	$⊢ v \in V$
17	15 16	xpex	$⊢ u \times v \in V$
18	17	rgen2w	$⊢ \forall u \in ran I \forall v \in ran I u \times v \in V$
19	18	mpocti	$⊢ (ran I ≼ ω \land ran I ≼ ω) \to (u \in ran I, v \in ran I ⟼ u \times v) ≼ ω$
20	3	breq1i	$⊢ R ≼ ω \leftrightarrow (u \in ran I, v \in ran I ⟼ u \times v) ≼ ω$
21	20	biimpri	$⊢ (u \in ran I, v \in ran I ⟼ u \times v) ≼ ω \to R ≼ ω$
22		rnct	$⊢ R ≼ ω \to ran R ≼ ω$
23	19 21 22	3syl	$⊢ (ran I ≼ ω \land ran I ≼ ω) \to ran R ≼ ω$
24	14 14 23	mp2an	$⊢ ran R ≼ ω$

Metamath Proof Explorer