Metamath Proof Explorer

Theorem dya2iocucvr

Description: The dyadic rectangular set collection covers ( RR X. RR ) . (Contributed by Thierry Arnoux, 18-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4 unissb ⊢ ( ∪ ran 𝑅 ⊆ ( ℝ × ℝ ) ↔ ∀ 𝑑 ∈ ran 𝑅 𝑑 ⊆ ( ℝ × ℝ ) )
5 vex ⊢ 𝑢 ∈ V
6 vex ⊢ 𝑣 ∈ V
7 5 6 xpex ⊢ ( 𝑢 × 𝑣 ) ∈ V
8 3 7 elrnmpo ⊢ ( 𝑑 ∈ ran 𝑅 ↔ ∃ 𝑢 ∈ ran 𝐼 ∃ 𝑣 ∈ ran 𝐼 𝑑 = ( 𝑢 × 𝑣 ) )
9 simpr ⊢ ( ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → 𝑑 = ( 𝑢 × 𝑣 ) )
10 pwssb ⊢ ( ran 𝐼 ⊆ 𝒫 ℝ ↔ ∀ 𝑑 ∈ ran 𝐼 𝑑 ⊆ ℝ )
11 ovex ⊢ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ V
12 2 11 elrnmpo ⊢ ( 𝑑 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
13 simpr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
14 simpll ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑥 ∈ ℤ )
15 14 zred ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑥 ∈ ℝ )
16 2re ⊢ 2 ∈ ℝ
17 16 a1i ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 2 ∈ ℝ )
18 2ne0 ⊢ 2 ≠ 0
19 18 a1i ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 2 ≠ 0 )
20 simplr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑛 ∈ ℤ )
21 17 19 20 reexpclzd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
22 2cnd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 2 ∈ ℂ )
23 22 19 20 expne0d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 2 ↑ 𝑛 ) ≠ 0 )
24 15 21 23 redivcld ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
25 1red ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 1 ∈ ℝ )
26 15 25 readdcld ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑥 + 1 ) ∈ ℝ )
27 26 21 23 redivcld ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
28 27 rexrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
29 icossre ⊢ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ) → ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ⊆ ℝ )
30 24 28 29 syl2anc ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ⊆ ℝ )
31 13 30 eqsstrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑑 ⊆ ℝ )
32 31 ex ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → 𝑑 ⊆ ℝ ) )
33 32 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → 𝑑 ⊆ ℝ )
34 12 33 sylbi ⊢ ( 𝑑 ∈ ran 𝐼 → 𝑑 ⊆ ℝ )
35 10 34 mprgbir ⊢ ran 𝐼 ⊆ 𝒫 ℝ
36 35 sseli ⊢ ( 𝑢 ∈ ran 𝐼 → 𝑢 ∈ 𝒫 ℝ )
37 36 elpwid ⊢ ( 𝑢 ∈ ran 𝐼 → 𝑢 ⊆ ℝ )
38 35 sseli ⊢ ( 𝑣 ∈ ran 𝐼 → 𝑣 ∈ 𝒫 ℝ )
39 38 elpwid ⊢ ( 𝑣 ∈ ran 𝐼 → 𝑣 ⊆ ℝ )
40 xpss12 ⊢ ( ( 𝑢 ⊆ ℝ ∧ 𝑣 ⊆ ℝ ) → ( 𝑢 × 𝑣 ) ⊆ ( ℝ × ℝ ) )
41 37 39 40 syl2an ⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( 𝑢 × 𝑣 ) ⊆ ( ℝ × ℝ ) )
42 41 adantr ⊢ ( ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ℝ × ℝ ) )
43 9 42 eqsstrd ⊢ ( ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → 𝑑 ⊆ ( ℝ × ℝ ) )
44 43 ex ⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( 𝑑 = ( 𝑢 × 𝑣 ) → 𝑑 ⊆ ( ℝ × ℝ ) ) )
45 44 rexlimivv ⊢ ( ∃ 𝑢 ∈ ran 𝐼 ∃ 𝑣 ∈ ran 𝐼 𝑑 = ( 𝑢 × 𝑣 ) → 𝑑 ⊆ ( ℝ × ℝ ) )
46 8 45 sylbi ⊢ ( 𝑑 ∈ ran 𝑅 → 𝑑 ⊆ ( ℝ × ℝ ) )
47 4 46 mprgbir ⊢ ∪ ran 𝑅 ⊆ ( ℝ × ℝ )
48 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
49 1 48 eqeltri ⊢ 𝐽 ∈ Top
50 49 49 txtopi ⊢ ( 𝐽 ×t 𝐽 ) ∈ Top
51 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
52 1 unieqi ⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
53 51 52 eqtr4i ⊢ ℝ = ∪ 𝐽
54 49 49 53 53 txunii ⊢ ( ℝ × ℝ ) = ∪ ( 𝐽 ×t 𝐽 )
55 54 topopn ⊢ ( ( 𝐽 ×t 𝐽 ) ∈ Top → ( ℝ × ℝ ) ∈ ( 𝐽 ×t 𝐽 ) )
56 1 2 3 dya2iocuni ⊢ ( ( ℝ × ℝ ) ∈ ( 𝐽 ×t 𝐽 ) → ∃ 𝑐 ∈ 𝒫 ran 𝑅 ∪ 𝑐 = ( ℝ × ℝ ) )
57 50 55 56 mp2b ⊢ ∃ 𝑐 ∈ 𝒫 ran 𝑅 ∪ 𝑐 = ( ℝ × ℝ )
58 simpr ⊢ ( ( 𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 = ( ℝ × ℝ ) ) → ∪ 𝑐 = ( ℝ × ℝ ) )
59 elpwi ⊢ ( 𝑐 ∈ 𝒫 ran 𝑅 → 𝑐 ⊆ ran 𝑅 )
60 59 adantr ⊢ ( ( 𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 = ( ℝ × ℝ ) ) → 𝑐 ⊆ ran 𝑅 )
61 60 unissd ⊢ ( ( 𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 = ( ℝ × ℝ ) ) → ∪ 𝑐 ⊆ ∪ ran 𝑅 )
62 58 61 eqsstrrd ⊢ ( ( 𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 = ( ℝ × ℝ ) ) → ( ℝ × ℝ ) ⊆ ∪ ran 𝑅 )
63 62 rexlimiva ⊢ ( ∃ 𝑐 ∈ 𝒫 ran 𝑅 ∪ 𝑐 = ( ℝ × ℝ ) → ( ℝ × ℝ ) ⊆ ∪ ran 𝑅 )
64 57 63 ax-mp ⊢ ( ℝ × ℝ ) ⊆ ∪ ran 𝑅
65 47 64 eqssi ⊢ ∪ ran 𝑅 = ( ℝ × ℝ )