Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
2 | | refsumcn.3 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | | refsumcn.4 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
4 | | refsumcn.5 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) |
5 | | refsumcn.2 |
. . . . . . . 8
⊢ 𝐾 = (topGen‘ran
(,)) |
6 | 1 | tgioo2 22414 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
7 | 5, 6 | eqtri 2632 |
. . . . . . 7
⊢ 𝐾 =
((TopOpen‘ℂfld) ↾t
ℝ) |
8 | 7 | oveq2i 6560 |
. . . . . 6
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)) |
9 | 4, 8 | syl6eleq 2698 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
10 | 1 | cnfldtopon 22396 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
12 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝑋)) |
13 | | retopon 22377 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
14 | 5, 13 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐾 ∈
(TopOn‘ℝ) |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐾 ∈
(TopOn‘ℝ)) |
16 | | cnf2 20863 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ℝ) ∧ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶ℝ) |
17 | 12, 15, 4, 16 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶ℝ) |
18 | | frn 5966 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶ℝ → ran (𝑥 ∈ 𝑋 ↦ 𝐵) ⊆ ℝ) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ran (𝑥 ∈ 𝑋 ↦ 𝐵) ⊆ ℝ) |
20 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ℝ ⊆
ℂ) |
22 | | cnrest2 20900 |
. . . . . 6
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑥 ∈ 𝑋 ↦ 𝐵) ⊆ ℝ ∧ ℝ ⊆
ℂ) → ((𝑥 ∈
𝑋 ↦ 𝐵) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
23 | 11, 19, 21, 22 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
24 | 9, 23 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
25 | 1, 2, 3, 24 | fsumcnf 38203 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
26 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
27 | | refsumcn.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝜑 |
28 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ Fin) |
29 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → 𝜑) |
30 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴) |
31 | 29, 30 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (𝜑 ∧ 𝑘 ∈ 𝐴)) |
32 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → 𝑥 ∈ 𝑋) |
33 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ 𝐵) |
34 | 33 | fmpt 6289 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝑋 𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶ℝ) |
35 | 17, 34 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∀𝑥 ∈ 𝑋 𝐵 ∈ ℝ) |
36 | | rsp 2913 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝑋 𝐵 ∈ ℝ → (𝑥 ∈ 𝑋 → 𝐵 ∈ ℝ)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 → 𝐵 ∈ ℝ)) |
38 | 31, 32, 37 | sylc 63 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
39 | 28, 38 | fsumrecl 14312 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
40 | 39 | ex 449 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)) |
41 | 27, 40 | ralrimi 2940 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
42 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) = (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) |
43 | 42 | fnmpt 5933 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑋 Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) Fn 𝑋) |
44 | 41, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) Fn 𝑋) |
45 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑋 |
46 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑦 |
47 | | nfmpt1 4675 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) |
48 | 45, 46, 47 | fvelrnbf 38200 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) Fn 𝑋 → (𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ↔ ∃𝑥 ∈ 𝑋 ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦)) |
49 | 44, 48 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ↔ ∃𝑥 ∈ 𝑋 ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦)) |
50 | 49 | biimpa 500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)) → ∃𝑥 ∈ 𝑋 ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) |
51 | 47 | nfrn 5289 |
. . . . . . . . . 10
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) |
52 | 51 | nfcri 2745 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) |
53 | 27, 52 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)) |
54 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥ℝ |
55 | 54 | nfcri 2745 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ∈ ℝ |
56 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
57 | 56, 39 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ 𝑋 ∧ Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)) |
58 | 42 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) → ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = Σ𝑘 ∈ 𝐴 𝐵) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = Σ𝑘 ∈ 𝐴 𝐵) |
60 | 59 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) → ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = Σ𝑘 ∈ 𝐴 𝐵) |
61 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) → ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) |
62 | 60, 61 | eqtr3d 2646 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) → Σ𝑘 ∈ 𝐴 𝐵 = 𝑦) |
63 | 39 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
64 | 62, 63 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) → 𝑦 ∈ ℝ) |
65 | 64 | 3adant1r 1311 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)) ∧ 𝑥 ∈ 𝑋 ∧ ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦) → 𝑦 ∈ ℝ) |
66 | 65 | 3exp 1256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)) → (𝑥 ∈ 𝑋 → (((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦 → 𝑦 ∈ ℝ))) |
67 | 53, 55, 66 | rexlimd 3008 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)) → (∃𝑥 ∈ 𝑋 ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)‘𝑥) = 𝑦 → 𝑦 ∈ ℝ)) |
68 | 50, 67 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵)) → 𝑦 ∈ ℝ) |
69 | 68 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) → 𝑦 ∈ ℝ)) |
70 | 69 | ssrdv 3574 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ⊆ ℝ) |
71 | 20 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ⊆
ℂ) |
72 | | cnrest2 20900 |
. . . 4
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ⊆ ℝ ∧ ℝ ⊆
ℂ) → ((𝑥 ∈
𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
73 | 26, 70, 71, 72 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
74 | 25, 73 | mpbid 221 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
75 | 74, 8 | syl6eleqr 2699 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾)) |