Metamath Proof Explorer

Theorem dya2iocuni

Description: Every open set of ( RR X. RR ) is a union of closed-below open-above dyadic rational rectangular subsets of ( RR X. RR ) . This union must be a countable union by dya2iocct . (Contributed by Thierry Arnoux, 18-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
dya2ioc.2 ⊢ R = u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v
Assertion dya2iocuni ⊢ A ∈ J × t J → ∃ c ∈ 𝒫 ran ⁡ R ⋃ c = A

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
2 dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
3 dya2ioc.2 ⊢ R = u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v
4 ssrab2 ⊢ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ⊆ ran ⁡ R
5 1 2 3 dya2iocrfn ⊢ R Fn ran ⁡ I × ran ⁡ I
6 zex ⊢ ℤ ∈ V
7 6 6 mpoex ⊢ x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n ∈ V
8 2 7 eqeltri ⊢ I ∈ V
9 8 rnex ⊢ ran ⁡ I ∈ V
10 9 9 xpex ⊢ ran ⁡ I × ran ⁡ I ∈ V
11 fnex ⊢ R Fn ran ⁡ I × ran ⁡ I ∧ ran ⁡ I × ran ⁡ I ∈ V → R ∈ V
12 5 10 11 mp2an ⊢ R ∈ V
13 12 rnex ⊢ ran ⁡ R ∈ V
14 13 elpw2 ⊢ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ∈ 𝒫 ran ⁡ R ↔ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ⊆ ran ⁡ R
15 4 14 mpbir ⊢ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ∈ 𝒫 ran ⁡ R
16 15 a1i ⊢ A ∈ J × t J → b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ∈ 𝒫 ran ⁡ R
17 rex0 ⊢ ¬ ∃ z ∈ ∅ z ∈ b ∧ b ⊆ A
18 rexeq ⊢ A = ∅ → ∃ z ∈ A z ∈ b ∧ b ⊆ A ↔ ∃ z ∈ ∅ z ∈ b ∧ b ⊆ A
19 17 18 mtbiri ⊢ A = ∅ → ¬ ∃ z ∈ A z ∈ b ∧ b ⊆ A
20 19 ralrimivw ⊢ A = ∅ → ∀ b ∈ ran ⁡ R ¬ ∃ z ∈ A z ∈ b ∧ b ⊆ A
21 rabeq0 ⊢ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A = ∅ ↔ ∀ b ∈ ran ⁡ R ¬ ∃ z ∈ A z ∈ b ∧ b ⊆ A
22 20 21 sylibr ⊢ A = ∅ → b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A = ∅
23 22 unieqd ⊢ A = ∅ → ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A = ⋃ ∅
24 uni0 ⊢ ⋃ ∅ = ∅
25 23 24 eqtrdi ⊢ A = ∅ → ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A = ∅
26 0ss ⊢ ∅ ⊆ A
27 25 26 eqsstrdi ⊢ A = ∅ → ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ⊆ A
28 elequ2 ⊢ b = p → z ∈ b ↔ z ∈ p
29 sseq1 ⊢ b = p → b ⊆ A ↔ p ⊆ A
30 28 29 anbi12d ⊢ b = p → z ∈ b ∧ b ⊆ A ↔ z ∈ p ∧ p ⊆ A
31 30 rexbidv ⊢ b = p → ∃ z ∈ A z ∈ b ∧ b ⊆ A ↔ ∃ z ∈ A z ∈ p ∧ p ⊆ A
32 31 elrab ⊢ p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ↔ p ∈ ran ⁡ R ∧ ∃ z ∈ A z ∈ p ∧ p ⊆ A
33 simpr ⊢ z ∈ p ∧ p ⊆ A → p ⊆ A
34 33 reximi ⊢ ∃ z ∈ A z ∈ p ∧ p ⊆ A → ∃ z ∈ A p ⊆ A
35 r19.9rzv ⊢ A ≠ ∅ → p ⊆ A ↔ ∃ z ∈ A p ⊆ A
36 34 35 imbitrrid ⊢ A ≠ ∅ → ∃ z ∈ A z ∈ p ∧ p ⊆ A → p ⊆ A
37 36 adantld ⊢ A ≠ ∅ → p ∈ ran ⁡ R ∧ ∃ z ∈ A z ∈ p ∧ p ⊆ A → p ⊆ A
38 32 37 biimtrid ⊢ A ≠ ∅ → p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A → p ⊆ A
39 38 ralrimiv ⊢ A ≠ ∅ → ∀ p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A p ⊆ A
40 unissb ⊢ ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ⊆ A ↔ ∀ p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A p ⊆ A
41 39 40 sylibr ⊢ A ≠ ∅ → ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ⊆ A
42 27 41 pm2.61ine ⊢ ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ⊆ A
43 42 a1i ⊢ A ∈ J × t J → ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ⊆ A
44 1 2 3 dya2iocnei ⊢ A ∈ J × t J ∧ m ∈ A → ∃ p ∈ ran ⁡ R m ∈ p ∧ p ⊆ A
45 simpl ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → p ∈ ran ⁡ R
46 ssel2 ⊢ p ⊆ A ∧ m ∈ p → m ∈ A
47 46 ancoms ⊢ m ∈ p ∧ p ⊆ A → m ∈ A
48 47 adantl ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → m ∈ A
49 simpr ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → m ∈ p ∧ p ⊆ A
50 elequ1 ⊢ z = m → z ∈ p ↔ m ∈ p
51 50 anbi1d ⊢ z = m → z ∈ p ∧ p ⊆ A ↔ m ∈ p ∧ p ⊆ A
52 51 rspcev ⊢ m ∈ A ∧ m ∈ p ∧ p ⊆ A → ∃ z ∈ A z ∈ p ∧ p ⊆ A
53 48 49 52 syl2anc ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → ∃ z ∈ A z ∈ p ∧ p ⊆ A
54 45 53 jca ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → p ∈ ran ⁡ R ∧ ∃ z ∈ A z ∈ p ∧ p ⊆ A
55 54 32 sylibr ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A
56 simprl ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → m ∈ p
57 55 56 jca ⊢ p ∈ ran ⁡ R ∧ m ∈ p ∧ p ⊆ A → p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ∧ m ∈ p
58 57 reximi2 ⊢ ∃ p ∈ ran ⁡ R m ∈ p ∧ p ⊆ A → ∃ p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A m ∈ p
59 44 58 syl ⊢ A ∈ J × t J ∧ m ∈ A → ∃ p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A m ∈ p
60 eluni2 ⊢ m ∈ ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ↔ ∃ p ∈ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A m ∈ p
61 59 60 sylibr ⊢ A ∈ J × t J ∧ m ∈ A → m ∈ ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A
62 43 61 eqelssd ⊢ A ∈ J × t J → ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A = A
63 unieq ⊢ c = b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A → ⋃ c = ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A
64 63 eqeq1d ⊢ c = b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A → ⋃ c = A ↔ ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A = A
65 64 rspcev ⊢ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A ∈ 𝒫 ran ⁡ R ∧ ⋃ b ∈ ran ⁡ R | ∃ z ∈ A z ∈ b ∧ b ⊆ A = A → ∃ c ∈ 𝒫 ran ⁡ R ⋃ c = A
66 16 62 65 syl2anc ⊢ A ∈ J × t J → ∃ c ∈ 𝒫 ran ⁡ R ⋃ c = A