| Step | Hyp | Ref
| Expression |
| 1 | | ima0 6095 |
. . . . . . . . 9
⊢ (𝑓 “ ∅) =
∅ |
| 2 | | 0ss 4400 |
. . . . . . . . 9
⊢ ∅
⊆ ∪ 𝑆 |
| 3 | 1, 2 | eqsstri 4030 |
. . . . . . . 8
⊢ (𝑓 “ ∅) ⊆ ∪ 𝑆 |
| 4 | 3 | a1i 11 |
. . . . . . 7
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (𝑓 “ ∅) ⊆ ∪ 𝑆) |
| 5 | 4 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
∀𝑓 ∈ (𝑅 Cn 𝑆)(𝑓 “ ∅) ⊆ ∪ 𝑆) |
| 6 | | rabid2 3470 |
. . . . . 6
⊢ ((𝑅 Cn 𝑆) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ ∅) ⊆ ∪ 𝑆}
↔ ∀𝑓 ∈
(𝑅 Cn 𝑆)(𝑓 “ ∅) ⊆ ∪ 𝑆) |
| 7 | 5, 6 | sylibr 234 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ ∅) ⊆ ∪ 𝑆}) |
| 8 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
| 9 | | simpl 482 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑅 ∈ Top) |
| 10 | | simpr 484 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top) |
| 11 | | 0ss 4400 |
. . . . . . 7
⊢ ∅
⊆ ∪ 𝑅 |
| 12 | 11 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∅
⊆ ∪ 𝑅) |
| 13 | | rest0 23177 |
. . . . . . . 8
⊢ (𝑅 ∈ Top → (𝑅 ↾t ∅) =
{∅}) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ↾t ∅) =
{∅}) |
| 15 | | 0cmp 23402 |
. . . . . . 7
⊢ {∅}
∈ Comp |
| 16 | 14, 15 | eqeltrdi 2849 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ↾t ∅)
∈ Comp) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝑆 =
∪ 𝑆 |
| 18 | 17 | topopn 22912 |
. . . . . . 7
⊢ (𝑆 ∈ Top → ∪ 𝑆
∈ 𝑆) |
| 19 | 18 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ 𝑆
∈ 𝑆) |
| 20 | 8, 9, 10, 12, 16, 19 | xkoopn 23597 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ ∅) ⊆ ∪ 𝑆}
∈ (𝑆
↑ko 𝑅)) |
| 21 | 7, 20 | eqeltrd 2841 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅)) |
| 22 | | xkouni.1 |
. . . 4
⊢ 𝐽 = (𝑆 ↑ko 𝑅) |
| 23 | 21, 22 | eleqtrrdi 2852 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ 𝐽) |
| 24 | | elssuni 4937 |
. . 3
⊢ ((𝑅 Cn 𝑆) ∈ 𝐽 → (𝑅 Cn 𝑆) ⊆ ∪ 𝐽) |
| 25 | 23, 24 | syl 17 |
. 2
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ ∪ 𝐽) |
| 26 | | eqid 2737 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp} = {𝑥 ∈
𝒫 ∪ 𝑅 ∣ (𝑅 ↾t 𝑥) ∈ Comp} |
| 27 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
| 28 | 8, 26, 27 | xkoval 23595 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) = (topGen‘(fi‘ran
(𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
| 29 | 28 | unieqd 4920 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ (𝑆
↑ko 𝑅) =
∪ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
| 30 | 22 | unieqi 4919 |
. . . 4
⊢ ∪ 𝐽 =
∪ (𝑆 ↑ko 𝑅) |
| 31 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑅 Cn 𝑆) ∈ V |
| 32 | 31 | pwex 5380 |
. . . . . . 7
⊢ 𝒫
(𝑅 Cn 𝑆) ∈ V |
| 33 | 8, 26, 27 | xkotf 23593 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}):({𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) |
| 34 | | frn 6743 |
. . . . . . . 8
⊢ ((𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}):({𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆)) |
| 35 | 33, 34 | ax-mp 5 |
. . . . . . 7
⊢ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆) |
| 36 | 32, 35 | ssexi 5322 |
. . . . . 6
⊢ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ∈ V |
| 37 | | fiuni 9468 |
. . . . . 6
⊢ (ran
(𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ∈ V → ∪ ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ∪
(fi‘ran (𝑘 ∈
{𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) |
| 38 | 36, 37 | ax-mp 5 |
. . . . 5
⊢ ∪ ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ∪
(fi‘ran (𝑘 ∈
{𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
| 39 | | fvex 6919 |
. . . . . 6
⊢
(fi‘ran (𝑘
∈ {𝑥 ∈ 𝒫
∪ 𝑅 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) ∈ V |
| 40 | | unitg 22974 |
. . . . . 6
⊢
((fi‘ran (𝑘
∈ {𝑥 ∈ 𝒫
∪ 𝑅 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) ∈ V → ∪ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) = ∪
(fi‘ran (𝑘 ∈
{𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) |
| 41 | 39, 40 | ax-mp 5 |
. . . . 5
⊢ ∪ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) = ∪
(fi‘ran (𝑘 ∈
{𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
| 42 | 38, 41 | eqtr4i 2768 |
. . . 4
⊢ ∪ ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ∪
(topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) |
| 43 | 29, 30, 42 | 3eqtr4g 2802 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ 𝐽 =
∪ ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
| 44 | 35 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆)) |
| 45 | | sspwuni 5100 |
. . . 4
⊢ (ran
(𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆) ↔ ∪ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (𝑅 Cn 𝑆)) |
| 46 | 44, 45 | sylib 218 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (𝑅 Cn 𝑆)) |
| 47 | 43, 46 | eqsstrd 4018 |
. 2
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ 𝐽
⊆ (𝑅 Cn 𝑆)) |
| 48 | 25, 47 | eqssd 4001 |
1
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ 𝐽) |