| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xkofvcn.2 | . 2
⊢ 𝐹 = (𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) | 
| 2 |  | nllytop 23481 | . . . 4
⊢ (𝑅 ∈ 𝑛-Locally Comp
→ 𝑅 ∈
Top) | 
| 3 |  | eqid 2737 | . . . . 5
⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅) | 
| 4 | 3 | xkotopon 23608 | . . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆))) | 
| 5 | 2, 4 | sylan 580 | . . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑆 ↑ko
𝑅) ∈
(TopOn‘(𝑅 Cn 𝑆))) | 
| 6 | 2 | adantr 480 | . . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑅 ∈
Top) | 
| 7 |  | xkofvcn.1 | . . . . 5
⊢ 𝑋 = ∪
𝑅 | 
| 8 | 7 | toptopon 22923 | . . . 4
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋)) | 
| 9 | 6, 8 | sylib 218 | . . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑅 ∈ (TopOn‘𝑋)) | 
| 10 | 5, 9 | cnmpt1st 23676 | . . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ 𝑓) ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn (𝑆 ↑ko 𝑅))) | 
| 11 | 5, 9 | cnmpt2nd 23677 | . . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn 𝑅)) | 
| 12 |  | 1on 8518 | . . . . . . 7
⊢
1o ∈ On | 
| 13 |  | distopon 23004 | . . . . . . 7
⊢
(1o ∈ On → 𝒫 1o ∈
(TopOn‘1o)) | 
| 14 | 12, 13 | mp1i 13 | . . . . . 6
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝒫 1o ∈ (TopOn‘1o)) | 
| 15 |  | xkoccn 23627 | . . . . . 6
⊢
((𝒫 1o ∈ (TopOn‘1o) ∧ 𝑅 ∈ (TopOn‘𝑋)) → (𝑦 ∈ 𝑋 ↦ (1o × {𝑦})) ∈ (𝑅 Cn (𝑅 ↑ko 𝒫
1o))) | 
| 16 | 14, 9, 15 | syl2anc 584 | . . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑦 ∈ 𝑋 ↦ (1o × {𝑦})) ∈ (𝑅 Cn (𝑅 ↑ko 𝒫
1o))) | 
| 17 |  | sneq 4636 | . . . . . 6
⊢ (𝑦 = 𝑥 → {𝑦} = {𝑥}) | 
| 18 | 17 | xpeq2d 5715 | . . . . 5
⊢ (𝑦 = 𝑥 → (1o × {𝑦}) = (1o ×
{𝑥})) | 
| 19 | 5, 9, 11, 9, 16, 18 | cnmpt21 23679 | . . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (1o × {𝑥})) ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn (𝑅 ↑ko 𝒫
1o))) | 
| 20 |  | distop 23002 | . . . . . 6
⊢
(1o ∈ On → 𝒫 1o ∈
Top) | 
| 21 | 12, 20 | mp1i 13 | . . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝒫 1o ∈ Top) | 
| 22 |  | eqid 2737 | . . . . . 6
⊢ (𝑅 ↑ko 𝒫
1o) = (𝑅
↑ko 𝒫 1o) | 
| 23 | 22 | xkotopon 23608 | . . . . 5
⊢
((𝒫 1o ∈ Top ∧ 𝑅 ∈ Top) → (𝑅 ↑ko 𝒫
1o) ∈ (TopOn‘(𝒫 1o Cn 𝑅))) | 
| 24 | 21, 6, 23 | syl2anc 584 | . . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑅 ↑ko
𝒫 1o) ∈ (TopOn‘(𝒫 1o Cn 𝑅))) | 
| 25 |  | simpl 482 | . . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑅 ∈ 𝑛-Locally
Comp) | 
| 26 |  | simpr 484 | . . . . 5
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝑆 ∈
Top) | 
| 27 |  | eqid 2737 | . . . . . 6
⊢ (𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1o Cn 𝑅) ↦ (𝑔 ∘ ℎ)) = (𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1o Cn 𝑅) ↦ (𝑔 ∘ ℎ)) | 
| 28 | 27 | xkococn 23668 | . . . . 5
⊢
((𝒫 1o ∈ Top ∧ 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top) → (𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1o Cn 𝑅) ↦ (𝑔 ∘ ℎ)) ∈ (((𝑆 ↑ko 𝑅) ×t (𝑅 ↑ko 𝒫
1o)) Cn (𝑆
↑ko 𝒫 1o))) | 
| 29 | 21, 25, 26, 28 | syl3anc 1373 | . . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑔 ∈ (𝑅 Cn 𝑆), ℎ ∈ (𝒫 1o Cn 𝑅) ↦ (𝑔 ∘ ℎ)) ∈ (((𝑆 ↑ko 𝑅) ×t (𝑅 ↑ko 𝒫
1o)) Cn (𝑆
↑ko 𝒫 1o))) | 
| 30 |  | coeq1 5868 | . . . . 5
⊢ (𝑔 = 𝑓 → (𝑔 ∘ ℎ) = (𝑓 ∘ ℎ)) | 
| 31 |  | coeq2 5869 | . . . . 5
⊢ (ℎ = (1o × {𝑥}) → (𝑓 ∘ ℎ) = (𝑓 ∘ (1o × {𝑥}))) | 
| 32 | 30, 31 | sylan9eq 2797 | . . . 4
⊢ ((𝑔 = 𝑓 ∧ ℎ = (1o × {𝑥})) → (𝑔 ∘ ℎ) = (𝑓 ∘ (1o × {𝑥}))) | 
| 33 | 5, 9, 10, 19, 5, 24, 29, 32 | cnmpt22 23682 | . . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓 ∘ (1o × {𝑥}))) ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn (𝑆 ↑ko 𝒫
1o))) | 
| 34 |  | eqid 2737 | . . . . 5
⊢ (𝑆 ↑ko 𝒫
1o) = (𝑆
↑ko 𝒫 1o) | 
| 35 | 34 | xkotopon 23608 | . . . 4
⊢
((𝒫 1o ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝒫
1o) ∈ (TopOn‘(𝒫 1o Cn 𝑆))) | 
| 36 | 21, 26, 35 | syl2anc 584 | . . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑆 ↑ko
𝒫 1o) ∈ (TopOn‘(𝒫 1o Cn 𝑆))) | 
| 37 |  | 0lt1o 8542 | . . . . 5
⊢ ∅
∈ 1o | 
| 38 | 37 | a1i 11 | . . . 4
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
∅ ∈ 1o) | 
| 39 |  | unipw 5455 | . . . . . 6
⊢ ∪ 𝒫 1o = 1o | 
| 40 | 39 | eqcomi 2746 | . . . . 5
⊢
1o = ∪ 𝒫
1o | 
| 41 | 40 | xkopjcn 23664 | . . . 4
⊢
((𝒫 1o ∈ Top ∧ 𝑆 ∈ Top ∧ ∅ ∈
1o) → (𝑔
∈ (𝒫 1o Cn 𝑆) ↦ (𝑔‘∅)) ∈ ((𝑆 ↑ko 𝒫
1o) Cn 𝑆)) | 
| 42 | 21, 26, 38, 41 | syl3anc 1373 | . . 3
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑔 ∈ (𝒫
1o Cn 𝑆) ↦
(𝑔‘∅)) ∈
((𝑆 ↑ko
𝒫 1o) Cn 𝑆)) | 
| 43 |  | fveq1 6905 | . . . 4
⊢ (𝑔 = (𝑓 ∘ (1o × {𝑥})) → (𝑔‘∅) = ((𝑓 ∘ (1o × {𝑥}))‘∅)) | 
| 44 |  | vex 3484 | . . . . . . 7
⊢ 𝑥 ∈ V | 
| 45 | 44 | fconst 6794 | . . . . . 6
⊢
(1o × {𝑥}):1o⟶{𝑥} | 
| 46 |  | fvco3 7008 | . . . . . 6
⊢
(((1o × {𝑥}):1o⟶{𝑥} ∧ ∅ ∈ 1o) →
((𝑓 ∘ (1o
× {𝑥}))‘∅) = (𝑓‘((1o × {𝑥})‘∅))) | 
| 47 | 45, 37, 46 | mp2an 692 | . . . . 5
⊢ ((𝑓 ∘ (1o ×
{𝑥}))‘∅) =
(𝑓‘((1o
× {𝑥})‘∅)) | 
| 48 | 44 | fvconst2 7224 | . . . . . . 7
⊢ (∅
∈ 1o → ((1o × {𝑥})‘∅) = 𝑥) | 
| 49 | 37, 48 | ax-mp 5 | . . . . . 6
⊢
((1o × {𝑥})‘∅) = 𝑥 | 
| 50 | 49 | fveq2i 6909 | . . . . 5
⊢ (𝑓‘((1o ×
{𝑥})‘∅)) =
(𝑓‘𝑥) | 
| 51 | 47, 50 | eqtri 2765 | . . . 4
⊢ ((𝑓 ∘ (1o ×
{𝑥}))‘∅) =
(𝑓‘𝑥) | 
| 52 | 43, 51 | eqtrdi 2793 | . . 3
⊢ (𝑔 = (𝑓 ∘ (1o × {𝑥})) → (𝑔‘∅) = (𝑓‘𝑥)) | 
| 53 | 5, 9, 33, 36, 42, 52 | cnmpt21 23679 | . 2
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
(𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn 𝑆)) | 
| 54 | 1, 53 | eqeltrid 2845 | 1
⊢ ((𝑅 ∈ 𝑛-Locally Comp
∧ 𝑆 ∈ Top) →
𝐹 ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn 𝑆)) |