Step |
Hyp |
Ref |
Expression |
1 |
|
sxbrsiga.0 |
⊢ 𝐽 = ( topGen ‘ ran (,) ) |
2 |
|
dya2ioc.1 |
⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
3 |
|
dya2ioc.2 |
⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) ) |
4 |
1 2 3
|
dya2iocucvr |
⊢ ∪ ran 𝑅 = ( ℝ × ℝ ) |
5 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
6 |
1 5
|
eqeltri |
⊢ 𝐽 ∈ Top |
7 |
|
uniretop |
⊢ ℝ = ∪ ( topGen ‘ ran (,) ) |
8 |
1
|
unieqi |
⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) ) |
9 |
7 8
|
eqtr4i |
⊢ ℝ = ∪ 𝐽 |
10 |
6 6 9 9
|
txunii |
⊢ ( ℝ × ℝ ) = ∪ ( 𝐽 ×t 𝐽 ) |
11 |
4 10
|
eqtr2i |
⊢ ∪ ( 𝐽 ×t 𝐽 ) = ∪ ran 𝑅 |
12 |
1 2 3
|
dya2iocuni |
⊢ ( 𝑥 ∈ ( 𝐽 ×t 𝐽 ) → ∃ 𝑦 ∈ 𝒫 ran 𝑅 ∪ 𝑦 = 𝑥 ) |
13 |
|
simpr |
⊢ ( ( 𝑦 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑦 = 𝑥 ) → ∪ 𝑦 = 𝑥 ) |
14 |
1 2 3
|
dya2iocct |
⊢ ran 𝑅 ≼ ω |
15 |
|
ctex |
⊢ ( ran 𝑅 ≼ ω → ran 𝑅 ∈ V ) |
16 |
14 15
|
mp1i |
⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → ran 𝑅 ∈ V ) |
17 |
|
elpwi |
⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → 𝑦 ⊆ ran 𝑅 ) |
18 |
|
ssct |
⊢ ( ( 𝑦 ⊆ ran 𝑅 ∧ ran 𝑅 ≼ ω ) → 𝑦 ≼ ω ) |
19 |
17 14 18
|
sylancl |
⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → 𝑦 ≼ ω ) |
20 |
|
elsigagen2 |
⊢ ( ( ran 𝑅 ∈ V ∧ 𝑦 ⊆ ran 𝑅 ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ ( sigaGen ‘ ran 𝑅 ) ) |
21 |
16 17 19 20
|
syl3anc |
⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → ∪ 𝑦 ∈ ( sigaGen ‘ ran 𝑅 ) ) |
22 |
21
|
adantr |
⊢ ( ( 𝑦 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑦 = 𝑥 ) → ∪ 𝑦 ∈ ( sigaGen ‘ ran 𝑅 ) ) |
23 |
13 22
|
eqeltrrd |
⊢ ( ( 𝑦 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑦 = 𝑥 ) → 𝑥 ∈ ( sigaGen ‘ ran 𝑅 ) ) |
24 |
23
|
rexlimiva |
⊢ ( ∃ 𝑦 ∈ 𝒫 ran 𝑅 ∪ 𝑦 = 𝑥 → 𝑥 ∈ ( sigaGen ‘ ran 𝑅 ) ) |
25 |
12 24
|
syl |
⊢ ( 𝑥 ∈ ( 𝐽 ×t 𝐽 ) → 𝑥 ∈ ( sigaGen ‘ ran 𝑅 ) ) |
26 |
25
|
ssriv |
⊢ ( 𝐽 ×t 𝐽 ) ⊆ ( sigaGen ‘ ran 𝑅 ) |
27 |
14 15
|
ax-mp |
⊢ ran 𝑅 ∈ V |
28 |
|
sigagenss2 |
⊢ ( ( ∪ ( 𝐽 ×t 𝐽 ) = ∪ ran 𝑅 ∧ ( 𝐽 ×t 𝐽 ) ⊆ ( sigaGen ‘ ran 𝑅 ) ∧ ran 𝑅 ∈ V ) → ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ran 𝑅 ) ) |
29 |
11 26 27 28
|
mp3an |
⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ran 𝑅 ) |