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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion dya2iocuni ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) → ∃ 𝑐 ∈ 𝒫 ran 𝑅 ∪ 𝑐 = 𝐴 )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4 ssrab2 ⊢ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ⊆ ran 𝑅
5 1 2 3 dya2iocrfn ⊢ 𝑅 Fn ( ran 𝐼 × ran 𝐼 )
6 zex ⊢ ℤ ∈ V
7 6 6 mpoex ⊢ ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ∈ V
8 2 7 eqeltri ⊢ 𝐼 ∈ V
9 8 rnex ⊢ ran 𝐼 ∈ V
10 9 9 xpex ⊢ ( ran 𝐼 × ran 𝐼 ) ∈ V
11 fnex ⊢ ( ( 𝑅 Fn ( ran 𝐼 × ran 𝐼 ) ∧ ( ran 𝐼 × ran 𝐼 ) ∈ V ) → 𝑅 ∈ V )
12 5 10 11 mp2an ⊢ 𝑅 ∈ V
13 12 rnex ⊢ ran 𝑅 ∈ V
14 13 elpw2 ⊢ ( { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ∈ 𝒫 ran 𝑅 ↔ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ⊆ ran 𝑅 )
15 4 14 mpbir ⊢ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ∈ 𝒫 ran 𝑅
16 15 a1i ⊢ ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) → { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ∈ 𝒫 ran 𝑅 )
17 rex0 ⊢ ¬ ∃ 𝑧 ∈ ∅ ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 )
18 rexeq ⊢ ( 𝐴 = ∅ → ( ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ↔ ∃ 𝑧 ∈ ∅ ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ) )
19 17 18 mtbiri ⊢ ( 𝐴 = ∅ → ¬ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
20 19 ralrimivw ⊢ ( 𝐴 = ∅ → ∀ 𝑏 ∈ ran 𝑅 ¬ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
21 rabeq0 ⊢ ( { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } = ∅ ↔ ∀ 𝑏 ∈ ran 𝑅 ¬ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
22 20 21 sylibr ⊢ ( 𝐴 = ∅ → { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } = ∅ )
23 22 unieqd ⊢ ( 𝐴 = ∅ → ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } = ∪ ∅ )
24 uni0 ⊢ ∪ ∅ = ∅
25 23 24 eqtrdi ⊢ ( 𝐴 = ∅ → ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } = ∅ )
26 0ss ⊢ ∅ ⊆ 𝐴
27 25 26 eqsstrdi ⊢ ( 𝐴 = ∅ → ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ⊆ 𝐴 )
28 elequ2 ⊢ ( 𝑏 = 𝑝 → ( 𝑧 ∈ 𝑏 ↔ 𝑧 ∈ 𝑝 ) )
29 sseq1 ⊢ ( 𝑏 = 𝑝 → ( 𝑏 ⊆ 𝐴 ↔ 𝑝 ⊆ 𝐴 ) )
30 28 29 anbi12d ⊢ ( 𝑏 = 𝑝 → ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ↔ ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) )
31 30 rexbidv ⊢ ( 𝑏 = 𝑝 → ( ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) )
32 31 elrab ⊢ ( 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ↔ ( 𝑝 ∈ ran 𝑅 ∧ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) )
33 simpr ⊢ ( ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) → 𝑝 ⊆ 𝐴 )
34 33 reximi ⊢ ( ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) → ∃ 𝑧 ∈ 𝐴 𝑝 ⊆ 𝐴 )
35 r19.9rzv ⊢ ( 𝐴 ≠ ∅ → ( 𝑝 ⊆ 𝐴 ↔ ∃ 𝑧 ∈ 𝐴 𝑝 ⊆ 𝐴 ) )
36 34 35 imbitrrid ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) → 𝑝 ⊆ 𝐴 ) )
37 36 adantld ⊢ ( 𝐴 ≠ ∅ → ( ( 𝑝 ∈ ran 𝑅 ∧ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑝 ⊆ 𝐴 ) )
38 32 37 biimtrid ⊢ ( 𝐴 ≠ ∅ → ( 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } → 𝑝 ⊆ 𝐴 ) )
39 38 ralrimiv ⊢ ( 𝐴 ≠ ∅ → ∀ 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } 𝑝 ⊆ 𝐴 )
40 unissb ⊢ ( ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ⊆ 𝐴 ↔ ∀ 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } 𝑝 ⊆ 𝐴 )
41 39 40 sylibr ⊢ ( 𝐴 ≠ ∅ → ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ⊆ 𝐴 )
42 27 41 pm2.61ine ⊢ ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ⊆ 𝐴
43 42 a1i ⊢ ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) → ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ⊆ 𝐴 )
44 1 2 3 dya2iocnei ⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑚 ∈ 𝐴 ) → ∃ 𝑝 ∈ ran 𝑅 ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) )
45 simpl ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑝 ∈ ran 𝑅 )
46 ssel2 ⊢ ( ( 𝑝 ⊆ 𝐴 ∧ 𝑚 ∈ 𝑝 ) → 𝑚 ∈ 𝐴 )
47 46 ancoms ⊢ ( ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) → 𝑚 ∈ 𝐴 )
48 47 adantl ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑚 ∈ 𝐴 )
49 simpr ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) )
50 elequ1 ⊢ ( 𝑧 = 𝑚 → ( 𝑧 ∈ 𝑝 ↔ 𝑚 ∈ 𝑝 ) )
51 50 anbi1d ⊢ ( 𝑧 = 𝑚 → ( ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ↔ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) )
52 51 rspcev ⊢ ( ( 𝑚 ∈ 𝐴 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) )
53 48 49 52 syl2anc ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) )
54 45 53 jca ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → ( 𝑝 ∈ ran 𝑅 ∧ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) )
55 54 32 sylibr ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } )
56 simprl ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑚 ∈ 𝑝 )
57 55 56 jca ⊢ ( ( 𝑝 ∈ ran 𝑅 ∧ ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) ) → ( 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ∧ 𝑚 ∈ 𝑝 ) )
58 57 reximi2 ⊢ ( ∃ 𝑝 ∈ ran 𝑅 ( 𝑚 ∈ 𝑝 ∧ 𝑝 ⊆ 𝐴 ) → ∃ 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } 𝑚 ∈ 𝑝 )
59 44 58 syl ⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑚 ∈ 𝐴 ) → ∃ 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } 𝑚 ∈ 𝑝 )
60 eluni2 ⊢ ( 𝑚 ∈ ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ↔ ∃ 𝑝 ∈ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } 𝑚 ∈ 𝑝 )
61 59 60 sylibr ⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } )
62 43 61 eqelssd ⊢ ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) → ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } = 𝐴 )
63 unieq ⊢ ( 𝑐 = { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } → ∪ 𝑐 = ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } )
64 63 eqeq1d ⊢ ( 𝑐 = { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } → ( ∪ 𝑐 = 𝐴 ↔ ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } = 𝐴 ) )
65 64 rspcev ⊢ ( ( { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } ∈ 𝒫 ran 𝑅 ∧ ∪ { 𝑏 ∈ ran 𝑅 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) } = 𝐴 ) → ∃ 𝑐 ∈ 𝒫 ran 𝑅 ∪ 𝑐 = 𝐴 )
66 16 62 65 syl2anc ⊢ ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) → ∃ 𝑐 ∈ 𝒫 ran 𝑅 ∪ 𝑐 = 𝐴 )