Step |
Hyp |
Ref |
Expression |
1 |
|
sxbrsiga.0 |
⊢ 𝐽 = ( topGen ‘ ran (,) ) |
2 |
|
sxbrsigalem0 |
⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ ) |
3 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
4 |
1 3
|
eqeltri |
⊢ 𝐽 ∈ Top |
5 |
4 4
|
txtopi |
⊢ ( 𝐽 ×t 𝐽 ) ∈ Top |
6 |
|
uniretop |
⊢ ℝ = ∪ ( topGen ‘ ran (,) ) |
7 |
1
|
unieqi |
⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) ) |
8 |
6 7
|
eqtr4i |
⊢ ℝ = ∪ 𝐽 |
9 |
4 4 8 8
|
txunii |
⊢ ( ℝ × ℝ ) = ∪ ( 𝐽 ×t 𝐽 ) |
10 |
5 9
|
unicls |
⊢ ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) = ( ℝ × ℝ ) |
11 |
2 10
|
eqtr4i |
⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) |
12 |
|
ovex |
⊢ ( 𝑒 [,) +∞ ) ∈ V |
13 |
|
reex |
⊢ ℝ ∈ V |
14 |
12 13
|
xpex |
⊢ ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ V |
15 |
|
eqid |
⊢ ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) = ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
16 |
14 15
|
fnmpti |
⊢ ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) Fn ℝ |
17 |
|
oveq1 |
⊢ ( 𝑒 = 𝑢 → ( 𝑒 [,) +∞ ) = ( 𝑢 [,) +∞ ) ) |
18 |
17
|
xpeq1d |
⊢ ( 𝑒 = 𝑢 → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( 𝑢 [,) +∞ ) × ℝ ) ) |
19 |
|
ovex |
⊢ ( 𝑢 [,) +∞ ) ∈ V |
20 |
19 13
|
xpex |
⊢ ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ V |
21 |
18 15 20
|
fvmpt |
⊢ ( 𝑢 ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) = ( ( 𝑢 [,) +∞ ) × ℝ ) ) |
22 |
|
icopnfcld |
⊢ ( 𝑢 ∈ ℝ → ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
23 |
1
|
fveq2i |
⊢ ( Clsd ‘ 𝐽 ) = ( Clsd ‘ ( topGen ‘ ran (,) ) ) |
24 |
22 23
|
eleqtrrdi |
⊢ ( 𝑢 ∈ ℝ → ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ) |
25 |
|
dif0 |
⊢ ( ℝ ∖ ∅ ) = ℝ |
26 |
|
0opn |
⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 ) |
27 |
4 26
|
ax-mp |
⊢ ∅ ∈ 𝐽 |
28 |
8
|
opncld |
⊢ ( ( 𝐽 ∈ Top ∧ ∅ ∈ 𝐽 ) → ( ℝ ∖ ∅ ) ∈ ( Clsd ‘ 𝐽 ) ) |
29 |
4 27 28
|
mp2an |
⊢ ( ℝ ∖ ∅ ) ∈ ( Clsd ‘ 𝐽 ) |
30 |
25 29
|
eqeltrri |
⊢ ℝ ∈ ( Clsd ‘ 𝐽 ) |
31 |
|
txcld |
⊢ ( ( ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ∧ ℝ ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
32 |
24 30 31
|
sylancl |
⊢ ( 𝑢 ∈ ℝ → ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
33 |
21 32
|
eqeltrd |
⊢ ( 𝑢 ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
34 |
33
|
rgen |
⊢ ∀ 𝑢 ∈ ℝ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) |
35 |
|
fnfvrnss |
⊢ ( ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) Fn ℝ ∧ ∀ 𝑢 ∈ ℝ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) → ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
36 |
16 34 35
|
mp2an |
⊢ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) |
37 |
|
ovex |
⊢ ( 𝑓 [,) +∞ ) ∈ V |
38 |
13 37
|
xpex |
⊢ ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ V |
39 |
|
eqid |
⊢ ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) = ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
40 |
38 39
|
fnmpti |
⊢ ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) Fn ℝ |
41 |
|
oveq1 |
⊢ ( 𝑓 = 𝑣 → ( 𝑓 [,) +∞ ) = ( 𝑣 [,) +∞ ) ) |
42 |
41
|
xpeq2d |
⊢ ( 𝑓 = 𝑣 → ( ℝ × ( 𝑓 [,) +∞ ) ) = ( ℝ × ( 𝑣 [,) +∞ ) ) ) |
43 |
|
ovex |
⊢ ( 𝑣 [,) +∞ ) ∈ V |
44 |
13 43
|
xpex |
⊢ ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ V |
45 |
42 39 44
|
fvmpt |
⊢ ( 𝑣 ∈ ℝ → ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) = ( ℝ × ( 𝑣 [,) +∞ ) ) ) |
46 |
|
icopnfcld |
⊢ ( 𝑣 ∈ ℝ → ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
47 |
46 23
|
eleqtrrdi |
⊢ ( 𝑣 ∈ ℝ → ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ) |
48 |
|
txcld |
⊢ ( ( ℝ ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ) → ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
49 |
30 47 48
|
sylancr |
⊢ ( 𝑣 ∈ ℝ → ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
50 |
45 49
|
eqeltrd |
⊢ ( 𝑣 ∈ ℝ → ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
51 |
50
|
rgen |
⊢ ∀ 𝑣 ∈ ℝ ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) |
52 |
|
fnfvrnss |
⊢ ( ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) Fn ℝ ∧ ∀ 𝑣 ∈ ℝ ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) → ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
53 |
40 51 52
|
mp2an |
⊢ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) |
54 |
36 53
|
unssi |
⊢ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) |
55 |
|
fvex |
⊢ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V |
56 |
|
sssigagen |
⊢ ( ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V → ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) ) |
57 |
55 56
|
ax-mp |
⊢ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
58 |
54 57
|
sstri |
⊢ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |
59 |
|
sigagenss2 |
⊢ ( ( ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∧ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) ∧ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V ) → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) ) |
60 |
11 58 55 59
|
mp3an |
⊢ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) |