Step | Hyp | Ref
| Expression |
1 | | xkofvcn.2 |
. 2
⊢ 𝐹 = (𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) |
2 | | nllytop 21086 |
. . . 4
⊢ (𝑅 ∈ 𝑛-Locally Comp
→ 𝑅 ∈
Top) |
3 | | eqid 2610 |
. . . . 5
⊢ (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅) |
4 | 3 | xkotopon 21213 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆))) |
5 | 2, 4 | sylan 487 |
. . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑆 ^ko
𝑅) ∈
(TopOn‘(𝑅 Cn 𝑆))) |
6 | 2 | adantr 480 |
. . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑅 ∈
Top) |
7 | | xkofvcn.1 |
. . . . 5
⊢ 𝑋 = ∪
𝑅 |
8 | 7 | toptopon 20548 |
. . . 4
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋)) |
9 | 6, 8 | sylib 207 |
. . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑅 ∈ (TopOn‘𝑋)) |
10 | 5, 9 | cnmpt1st 21281 |
. . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ 𝑓) ∈ (((𝑆 ^ko 𝑅) ×t 𝑅) Cn (𝑆 ^ko 𝑅))) |
11 | 5, 9 | cnmpt2nd 21282 |
. . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (((𝑆 ^ko 𝑅) ×t 𝑅) Cn 𝑅)) |
12 | | 1on 7454 |
. . . . . . 7
⊢
1𝑜 ∈ On |
13 | | distopon 20611 |
. . . . . . 7
⊢
(1𝑜 ∈ On → 𝒫 1𝑜
∈ (TopOn‘1𝑜)) |
14 | 12, 13 | mp1i 13 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝒫 1𝑜 ∈
(TopOn‘1𝑜)) |
15 | | xkoccn 21232 |
. . . . . 6
⊢
((𝒫 1𝑜 ∈
(TopOn‘1𝑜) ∧ 𝑅 ∈ (TopOn‘𝑋)) → (𝑦 ∈ 𝑋 ↦ (1𝑜 ×
{𝑦})) ∈ (𝑅 Cn (𝑅 ^ko 𝒫
1𝑜))) |
16 | 14, 9, 15 | syl2anc 691 |
. . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑦 ∈ 𝑋 ↦ (1𝑜 ×
{𝑦})) ∈ (𝑅 Cn (𝑅 ^ko 𝒫
1𝑜))) |
17 | | sneq 4135 |
. . . . . 6
⊢ (𝑦 = 𝑥 → {𝑦} = {𝑥}) |
18 | 17 | xpeq2d 5063 |
. . . . 5
⊢ (𝑦 = 𝑥 → (1𝑜 × {𝑦}) = (1𝑜
× {𝑥})) |
19 | 5, 9, 11, 9, 16, 18 | cnmpt21 21284 |
. . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (1𝑜 ×
{𝑥})) ∈ (((𝑆 ^ko 𝑅) ×t 𝑅) Cn (𝑅 ^ko 𝒫
1𝑜))) |
20 | | distop 20610 |
. . . . . 6
⊢
(1𝑜 ∈ On → 𝒫 1𝑜
∈ Top) |
21 | 12, 20 | mp1i 13 |
. . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝒫 1𝑜 ∈ Top) |
22 | | eqid 2610 |
. . . . . 6
⊢ (𝑅 ^ko 𝒫
1𝑜) = (𝑅
^ko 𝒫 1𝑜) |
23 | 22 | xkotopon 21213 |
. . . . 5
⊢
((𝒫 1𝑜 ∈ Top ∧ 𝑅 ∈ Top) → (𝑅 ^ko 𝒫
1𝑜) ∈ (TopOn‘(𝒫 1𝑜 Cn
𝑅))) |
24 | 21, 6, 23 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑅 ^ko
𝒫 1𝑜) ∈ (TopOn‘(𝒫
1𝑜 Cn 𝑅))) |
25 | | simpl 472 |
. . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑅 ∈ 𝑛-Locally
Comp) |
26 | | simpr 476 |
. . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑆 ∈
Top) |
27 | | eqid 2610 |
. . . . . 6
⊢ (𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1𝑜 Cn
𝑅) ↦ (𝑔 ∘ ℎ)) = (𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1𝑜 Cn
𝑅) ↦ (𝑔 ∘ ℎ)) |
28 | 27 | xkococn 21273 |
. . . . 5
⊢
((𝒫 1𝑜 ∈ Top ∧ 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top) → (𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1𝑜 Cn
𝑅) ↦ (𝑔 ∘ ℎ)) ∈ (((𝑆 ^ko 𝑅) ×t (𝑅 ^ko 𝒫
1𝑜)) Cn (𝑆 ^ko 𝒫
1𝑜))) |
29 | 21, 25, 26, 28 | syl3anc 1318 |
. . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1𝑜 Cn
𝑅) ↦ (𝑔 ∘ ℎ)) ∈ (((𝑆 ^ko 𝑅) ×t (𝑅 ^ko 𝒫
1𝑜)) Cn (𝑆 ^ko 𝒫
1𝑜))) |
30 | | coeq1 5201 |
. . . . 5
⊢ (𝑔 = 𝑓 → (𝑔 ∘ ℎ) = (𝑓 ∘ ℎ)) |
31 | | coeq2 5202 |
. . . . 5
⊢ (ℎ = (1𝑜 ×
{𝑥}) → (𝑓 ∘ ℎ) = (𝑓 ∘ (1𝑜 ×
{𝑥}))) |
32 | 30, 31 | sylan9eq 2664 |
. . . 4
⊢ ((𝑔 = 𝑓 ∧ ℎ = (1𝑜 × {𝑥})) → (𝑔 ∘ ℎ) = (𝑓 ∘ (1𝑜 ×
{𝑥}))) |
33 | 5, 9, 10, 19, 5, 24, 29, 32 | cnmpt22 21287 |
. . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓 ∘ (1𝑜 ×
{𝑥}))) ∈ (((𝑆 ^ko 𝑅) ×t 𝑅) Cn (𝑆 ^ko 𝒫
1𝑜))) |
34 | | eqid 2610 |
. . . . 5
⊢ (𝑆 ^ko 𝒫
1𝑜) = (𝑆
^ko 𝒫 1𝑜) |
35 | 34 | xkotopon 21213 |
. . . 4
⊢
((𝒫 1𝑜 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝒫
1𝑜) ∈ (TopOn‘(𝒫 1𝑜 Cn
𝑆))) |
36 | 21, 26, 35 | syl2anc 691 |
. . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑆 ^ko
𝒫 1𝑜) ∈ (TopOn‘(𝒫
1𝑜 Cn 𝑆))) |
37 | | 0lt1o 7471 |
. . . . 5
⊢ ∅
∈ 1𝑜 |
38 | 37 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
∅ ∈ 1𝑜) |
39 | | unipw 4845 |
. . . . . 6
⊢ ∪ 𝒫 1𝑜 =
1𝑜 |
40 | 39 | eqcomi 2619 |
. . . . 5
⊢
1𝑜 = ∪ 𝒫
1𝑜 |
41 | 40 | xkopjcn 21269 |
. . . 4
⊢
((𝒫 1𝑜 ∈ Top ∧ 𝑆 ∈ Top ∧ ∅ ∈
1𝑜) → (𝑔 ∈ (𝒫 1𝑜 Cn
𝑆) ↦ (𝑔‘∅)) ∈ ((𝑆 ^ko 𝒫
1𝑜) Cn 𝑆)) |
42 | 21, 26, 38, 41 | syl3anc 1318 |
. . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑔 ∈ (𝒫
1𝑜 Cn 𝑆)
↦ (𝑔‘∅))
∈ ((𝑆
^ko 𝒫 1𝑜) Cn 𝑆)) |
43 | | fveq1 6102 |
. . . 4
⊢ (𝑔 = (𝑓 ∘ (1𝑜 ×
{𝑥})) → (𝑔‘∅) = ((𝑓 ∘ (1𝑜
× {𝑥}))‘∅)) |
44 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
45 | 44 | fconst 6004 |
. . . . . 6
⊢
(1𝑜 × {𝑥}):1𝑜⟶{𝑥} |
46 | | fvco3 6185 |
. . . . . 6
⊢
(((1𝑜 × {𝑥}):1𝑜⟶{𝑥} ∧ ∅ ∈
1𝑜) → ((𝑓 ∘ (1𝑜 ×
{𝑥}))‘∅) =
(𝑓‘((1𝑜 × {𝑥})‘∅))) |
47 | 45, 37, 46 | mp2an 704 |
. . . . 5
⊢ ((𝑓 ∘ (1𝑜
× {𝑥}))‘∅) = (𝑓‘((1𝑜 × {𝑥})‘∅)) |
48 | 44 | fvconst2 6374 |
. . . . . . 7
⊢ (∅
∈ 1𝑜 → ((1𝑜 × {𝑥})‘∅) = 𝑥) |
49 | 37, 48 | ax-mp 5 |
. . . . . 6
⊢
((1𝑜 × {𝑥})‘∅) = 𝑥 |
50 | 49 | fveq2i 6106 |
. . . . 5
⊢ (𝑓‘((1𝑜
× {𝑥})‘∅)) = (𝑓‘𝑥) |
51 | 47, 50 | eqtri 2632 |
. . . 4
⊢ ((𝑓 ∘ (1𝑜
× {𝑥}))‘∅) = (𝑓‘𝑥) |
52 | 43, 51 | syl6eq 2660 |
. . 3
⊢ (𝑔 = (𝑓 ∘ (1𝑜 ×
{𝑥})) → (𝑔‘∅) = (𝑓‘𝑥)) |
53 | 5, 9, 33, 36, 42, 52 | cnmpt21 21284 |
. 2
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ∈ (((𝑆 ^ko 𝑅) ×t 𝑅) Cn 𝑆)) |
54 | 1, 53 | syl5eqel 2692 |
1
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝐹 ∈ (((𝑆 ^ko 𝑅) ×t 𝑅) Cn 𝑆)) |