| Step | Hyp | Ref
| Expression |
| 1 | | sxbrsigalem0 34273 |
. . 3
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (ℝ ×
ℝ) |
| 2 | | sxbrsiga.0 |
. . . . . 6
⊢ 𝐽 = (topGen‘ran
(,)) |
| 3 | | retop 24782 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ Top |
| 4 | 2, 3 | eqeltri 2837 |
. . . . 5
⊢ 𝐽 ∈ Top |
| 5 | 4, 4 | txtopi 23598 |
. . . 4
⊢ (𝐽 ×t 𝐽) ∈ Top |
| 6 | | uniretop 24783 |
. . . . . 6
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 7 | 2 | unieqi 4919 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ (topGen‘ran (,)) |
| 8 | 6, 7 | eqtr4i 2768 |
. . . . 5
⊢ ℝ =
∪ 𝐽 |
| 9 | 4, 4, 8, 8 | txunii 23601 |
. . . 4
⊢ (ℝ
× ℝ) = ∪ (𝐽 ×t 𝐽) |
| 10 | 5, 9 | unicls 33902 |
. . 3
⊢ ∪ (Clsd‘(𝐽 ×t 𝐽)) = (ℝ ×
ℝ) |
| 11 | 1, 10 | eqtr4i 2768 |
. 2
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = ∪ (Clsd‘(𝐽 ×t 𝐽)) |
| 12 | | ovex 7464 |
. . . . . . 7
⊢ (𝑒[,)+∞) ∈
V |
| 13 | | reex 11246 |
. . . . . . 7
⊢ ℝ
∈ V |
| 14 | 12, 13 | xpex 7773 |
. . . . . 6
⊢ ((𝑒[,)+∞) × ℝ)
∈ V |
| 15 | | eqid 2737 |
. . . . . 6
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) =
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
| 16 | 14, 15 | fnmpti 6711 |
. . . . 5
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
Fn ℝ |
| 17 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑒 = 𝑢 → (𝑒[,)+∞) = (𝑢[,)+∞)) |
| 18 | 17 | xpeq1d 5714 |
. . . . . . . 8
⊢ (𝑒 = 𝑢 → ((𝑒[,)+∞) × ℝ) = ((𝑢[,)+∞) ×
ℝ)) |
| 19 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑢[,)+∞) ∈
V |
| 20 | 19, 13 | xpex 7773 |
. . . . . . . 8
⊢ ((𝑢[,)+∞) × ℝ)
∈ V |
| 21 | 18, 15, 20 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑢 ∈ ℝ → ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘𝑢) =
((𝑢[,)+∞) ×
ℝ)) |
| 22 | | icopnfcld 24788 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℝ → (𝑢[,)+∞) ∈
(Clsd‘(topGen‘ran (,)))) |
| 23 | 2 | fveq2i 6909 |
. . . . . . . . 9
⊢
(Clsd‘𝐽) =
(Clsd‘(topGen‘ran (,))) |
| 24 | 22, 23 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (𝑢 ∈ ℝ → (𝑢[,)+∞) ∈
(Clsd‘𝐽)) |
| 25 | | dif0 4378 |
. . . . . . . . 9
⊢ (ℝ
∖ ∅) = ℝ |
| 26 | | 0opn 22910 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Top → ∅
∈ 𝐽) |
| 27 | 4, 26 | ax-mp 5 |
. . . . . . . . . 10
⊢ ∅
∈ 𝐽 |
| 28 | 8 | opncld 23041 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ ∅ ∈
𝐽) → (ℝ ∖
∅) ∈ (Clsd‘𝐽)) |
| 29 | 4, 27, 28 | mp2an 692 |
. . . . . . . . 9
⊢ (ℝ
∖ ∅) ∈ (Clsd‘𝐽) |
| 30 | 25, 29 | eqeltrri 2838 |
. . . . . . . 8
⊢ ℝ
∈ (Clsd‘𝐽) |
| 31 | | txcld 23611 |
. . . . . . . 8
⊢ (((𝑢[,)+∞) ∈
(Clsd‘𝐽) ∧
ℝ ∈ (Clsd‘𝐽)) → ((𝑢[,)+∞) × ℝ) ∈
(Clsd‘(𝐽
×t 𝐽))) |
| 32 | 24, 30, 31 | sylancl 586 |
. . . . . . 7
⊢ (𝑢 ∈ ℝ → ((𝑢[,)+∞) × ℝ)
∈ (Clsd‘(𝐽
×t 𝐽))) |
| 33 | 21, 32 | eqeltrd 2841 |
. . . . . 6
⊢ (𝑢 ∈ ℝ → ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘𝑢) ∈
(Clsd‘(𝐽
×t 𝐽))) |
| 34 | 33 | rgen 3063 |
. . . . 5
⊢
∀𝑢 ∈
ℝ ((𝑒 ∈ ℝ
↦ ((𝑒[,)+∞)
× ℝ))‘𝑢)
∈ (Clsd‘(𝐽
×t 𝐽)) |
| 35 | | fnfvrnss 7141 |
. . . . 5
⊢ (((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
Fn ℝ ∧ ∀𝑢
∈ ℝ ((𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ))‘𝑢) ∈ (Clsd‘(𝐽 ×t 𝐽))) → ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
⊆ (Clsd‘(𝐽
×t 𝐽))) |
| 36 | 16, 34, 35 | mp2an 692 |
. . . 4
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ⊆ (Clsd‘(𝐽 ×t 𝐽)) |
| 37 | | ovex 7464 |
. . . . . . 7
⊢ (𝑓[,)+∞) ∈
V |
| 38 | 13, 37 | xpex 7773 |
. . . . . 6
⊢ (ℝ
× (𝑓[,)+∞))
∈ V |
| 39 | | eqid 2737 |
. . . . . 6
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) =
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) |
| 40 | 38, 39 | fnmpti 6711 |
. . . . 5
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) Fn
ℝ |
| 41 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑓 = 𝑣 → (𝑓[,)+∞) = (𝑣[,)+∞)) |
| 42 | 41 | xpeq2d 5715 |
. . . . . . . 8
⊢ (𝑓 = 𝑣 → (ℝ × (𝑓[,)+∞)) = (ℝ × (𝑣[,)+∞))) |
| 43 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑣[,)+∞) ∈
V |
| 44 | 13, 43 | xpex 7773 |
. . . . . . . 8
⊢ (ℝ
× (𝑣[,)+∞))
∈ V |
| 45 | 42, 39, 44 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑣 ∈ ℝ → ((𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞)))‘𝑣) = (ℝ × (𝑣[,)+∞))) |
| 46 | | icopnfcld 24788 |
. . . . . . . . 9
⊢ (𝑣 ∈ ℝ → (𝑣[,)+∞) ∈
(Clsd‘(topGen‘ran (,)))) |
| 47 | 46, 23 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (𝑣 ∈ ℝ → (𝑣[,)+∞) ∈
(Clsd‘𝐽)) |
| 48 | | txcld 23611 |
. . . . . . . 8
⊢ ((ℝ
∈ (Clsd‘𝐽) ∧
(𝑣[,)+∞) ∈
(Clsd‘𝐽)) →
(ℝ × (𝑣[,)+∞)) ∈ (Clsd‘(𝐽 ×t 𝐽))) |
| 49 | 30, 47, 48 | sylancr 587 |
. . . . . . 7
⊢ (𝑣 ∈ ℝ → (ℝ
× (𝑣[,)+∞))
∈ (Clsd‘(𝐽
×t 𝐽))) |
| 50 | 45, 49 | eqeltrd 2841 |
. . . . . 6
⊢ (𝑣 ∈ ℝ → ((𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞)))‘𝑣) ∈ (Clsd‘(𝐽 ×t 𝐽))) |
| 51 | 50 | rgen 3063 |
. . . . 5
⊢
∀𝑣 ∈
ℝ ((𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))‘𝑣) ∈ (Clsd‘(𝐽 ×t 𝐽)) |
| 52 | | fnfvrnss 7141 |
. . . . 5
⊢ (((𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) Fn
ℝ ∧ ∀𝑣
∈ ℝ ((𝑓 ∈
ℝ ↦ (ℝ × (𝑓[,)+∞)))‘𝑣) ∈ (Clsd‘(𝐽 ×t 𝐽))) → ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) ⊆
(Clsd‘(𝐽
×t 𝐽))) |
| 53 | 40, 51, 52 | mp2an 692 |
. . . 4
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ⊆ (Clsd‘(𝐽 ×t 𝐽)) |
| 54 | 36, 53 | unssi 4191 |
. . 3
⊢ (ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ⊆ (Clsd‘(𝐽 ×t 𝐽)) |
| 55 | | fvex 6919 |
. . . 4
⊢
(Clsd‘(𝐽
×t 𝐽))
∈ V |
| 56 | | sssigagen 34146 |
. . . 4
⊢
((Clsd‘(𝐽
×t 𝐽))
∈ V → (Clsd‘(𝐽 ×t 𝐽)) ⊆ (sigaGen‘(Clsd‘(𝐽 ×t 𝐽)))) |
| 57 | 55, 56 | ax-mp 5 |
. . 3
⊢
(Clsd‘(𝐽
×t 𝐽))
⊆ (sigaGen‘(Clsd‘(𝐽 ×t 𝐽))) |
| 58 | 54, 57 | sstri 3993 |
. 2
⊢ (ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ⊆
(sigaGen‘(Clsd‘(𝐽 ×t 𝐽))) |
| 59 | | sigagenss2 34151 |
. 2
⊢ ((∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = ∪ (Clsd‘(𝐽 ×t 𝐽)) ∧ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆
(sigaGen‘(Clsd‘(𝐽 ×t 𝐽))) ∧ (Clsd‘(𝐽 ×t 𝐽)) ∈ V) → (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ⊆
(sigaGen‘(Clsd‘(𝐽 ×t 𝐽)))) |
| 60 | 11, 58, 55, 59 | mp3an 1463 |
1
⊢
(sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ⊆
(sigaGen‘(Clsd‘(𝐽 ×t 𝐽))) |