Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . . 7
⊢ (𝑅 Cn 𝑆) ∈ V |
2 | 1 | pwex 4848 |
. . . . . 6
⊢ 𝒫
(𝑅 Cn 𝑆) ∈ V |
3 | | xkoopn.x |
. . . . . . . 8
⊢ 𝑋 = ∪
𝑅 |
4 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} |
5 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
6 | 3, 4, 5 | xkotf 21388 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}):({𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) |
7 | | frn 6053 |
. . . . . . 7
⊢ ((𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}):({𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆)) |
8 | 6, 7 | ax-mp 5 |
. . . . . 6
⊢ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆) |
9 | 2, 8 | ssexi 4803 |
. . . . 5
⊢ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ∈ V |
10 | | ssfii 8325 |
. . . . 5
⊢ (ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ∈ V → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) |
11 | 9, 10 | ax-mp 5 |
. . . 4
⊢ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
12 | | fvex 6201 |
. . . . 5
⊢
(fi‘ran (𝑘
∈ {𝑥 ∈ 𝒫
𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) ∈ V |
13 | | bastg 20770 |
. . . . 5
⊢
((fi‘ran (𝑘
∈ {𝑥 ∈ 𝒫
𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) ∈ V → (fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) ⊆ (topGen‘(fi‘ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
14 | 12, 13 | ax-mp 5 |
. . . 4
⊢
(fi‘ran (𝑘
∈ {𝑥 ∈ 𝒫
𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) ⊆ (topGen‘(fi‘ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) |
15 | 11, 14 | sstri 3612 |
. . 3
⊢ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) |
16 | | xkoopn.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
17 | | xkoopn.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Top) |
18 | 3 | topopn 20711 |
. . . . . . . 8
⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅) |
19 | | elpw2g 4827 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑅 → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋)) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋)) |
21 | 16, 20 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝑋) |
22 | | xkoopn.c |
. . . . . 6
⊢ (𝜑 → (𝑅 ↾t 𝐴) ∈ Comp) |
23 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑅 ↾t 𝑥) = (𝑅 ↾t 𝐴)) |
24 | 23 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑅 ↾t 𝑥) ∈ Comp ↔ (𝑅 ↾t 𝐴) ∈ Comp)) |
25 | 24 | elrab 3363 |
. . . . . 6
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} ↔ (𝐴 ∈ 𝒫 𝑋 ∧ (𝑅 ↾t 𝐴) ∈ Comp)) |
26 | 21, 22, 25 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}) |
27 | | xkoopn.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
28 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈}) |
29 | | imaeq2 5462 |
. . . . . . . . 9
⊢ (𝑘 = 𝐴 → (𝑓 “ 𝑘) = (𝑓 “ 𝐴)) |
30 | 29 | sseq1d 3632 |
. . . . . . . 8
⊢ (𝑘 = 𝐴 → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ (𝑓 “ 𝐴) ⊆ 𝑣)) |
31 | 30 | rabbidv 3189 |
. . . . . . 7
⊢ (𝑘 = 𝐴 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑣}) |
32 | 31 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑘 = 𝐴 → ({𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ↔ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑣})) |
33 | | sseq2 3627 |
. . . . . . . 8
⊢ (𝑣 = 𝑈 → ((𝑓 “ 𝐴) ⊆ 𝑣 ↔ (𝑓 “ 𝐴) ⊆ 𝑈)) |
34 | 33 | rabbidv 3189 |
. . . . . . 7
⊢ (𝑣 = 𝑈 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑣} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈}) |
35 | 34 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑣 = 𝑈 → ({𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑣} ↔ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈})) |
36 | 32, 35 | rspc2ev 3324 |
. . . . 5
⊢ ((𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} ∧ 𝑈 ∈ 𝑆 ∧ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈}) → ∃𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}∃𝑣 ∈ 𝑆 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
37 | 26, 27, 28, 36 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → ∃𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}∃𝑣 ∈ 𝑆 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
38 | 1 | rabex 4813 |
. . . . 5
⊢ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ V |
39 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} → (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ↔ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
40 | 39 | 2rexbidv 3057 |
. . . . 5
⊢ (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} → (∃𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}∃𝑣 ∈ 𝑆 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ↔ ∃𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}∃𝑣 ∈ 𝑆 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
41 | 5 | rnmpt2 6770 |
. . . . 5
⊢ ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑦 ∣ ∃𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}∃𝑣 ∈ 𝑆 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} |
42 | 38, 40, 41 | elab2 3354 |
. . . 4
⊢ ({𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ↔ ∃𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}∃𝑣 ∈ 𝑆 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
43 | 37, 42 | sylibr 224 |
. . 3
⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
44 | 15, 43 | sseldi 3601 |
. 2
⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
45 | | xkoopn.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ Top) |
46 | 3, 4, 5 | xkoval 21390 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) = (topGen‘(fi‘ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
47 | 17, 45, 46 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝑆 ^ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
48 | 44, 47 | eleqtrrd 2704 |
1
⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ (𝑆 ^ko 𝑅)) |