Theorem dya2iocct

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

	Ref	Expression
Hypotheses	sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
	dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
	dya2ioc.2	⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion	dya2iocct	⊢ ran 𝑅 ≼ ω

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3		dya2ioc.2	⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4		znnen	⊢ ℤ ≈ ℕ
5		nnct	⊢ ℕ ≼ ω
6		endomtr	⊢ ( ( ℤ ≈ ℕ ∧ ℕ ≼ ω ) → ℤ ≼ ω )
7	4 5 6	mp2an	⊢ ℤ ≼ ω
8		ovex	⊢ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ V
9	8	rgen2w	⊢ ∀ 𝑥 ∈ ℤ ∀ 𝑛 ∈ ℤ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ V
10	9	mpocti	⊢ ( ( ℤ ≼ ω ∧ ℤ ≼ ω ) → ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ≼ ω )
11	7 7 10	mp2an	⊢ ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ≼ ω
12	2 11	eqbrtri	⊢ 𝐼 ≼ ω
13		rnct	⊢ ( 𝐼 ≼ ω → ran 𝐼 ≼ ω )
14	12 13	ax-mp	⊢ ran 𝐼 ≼ ω
15		vex	⊢ 𝑢 ∈ V
16		vex	⊢ 𝑣 ∈ V
17	15 16	xpex	⊢ ( 𝑢 × 𝑣 ) ∈ V
18	17	rgen2w	⊢ ∀ 𝑢 ∈ ran 𝐼 ∀ 𝑣 ∈ ran 𝐼 ( 𝑢 × 𝑣 ) ∈ V
19	18	mpocti	⊢ ( ( ran 𝐼 ≼ ω ∧ ran 𝐼 ≼ ω ) → ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) ) ≼ ω )
20	3	breq1i	⊢ ( 𝑅 ≼ ω ↔ ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) ) ≼ ω )
21	20	biimpri	⊢ ( ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) ) ≼ ω → 𝑅 ≼ ω )
22		rnct	⊢ ( 𝑅 ≼ ω → ran 𝑅 ≼ ω )
23	19 21 22	3syl	⊢ ( ( ran 𝐼 ≼ ω ∧ ran 𝐼 ≼ ω ) → ran 𝑅 ≼ ω )
24	14 14 23	mp2an	⊢ ran 𝑅 ≼ ω