Step |
Hyp |
Ref |
Expression |
1 |
|
cncfmpt2f.1 |
⊢ 𝐽 = ( TopOpen ‘ ℂfld ) |
2 |
|
cncfmpt2f.2 |
⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
3 |
|
cncfmpt2f.3 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) ) |
4 |
|
cncfmpt2f.4 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) ) |
5 |
1
|
cnfldtopon |
⊢ 𝐽 ∈ ( TopOn ‘ ℂ ) |
6 |
|
cncfrss |
⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) → 𝑋 ⊆ ℂ ) |
7 |
3 6
|
syl |
⊢ ( 𝜑 → 𝑋 ⊆ ℂ ) |
8 |
|
resttopon |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) ) |
9 |
5 7 8
|
sylancr |
⊢ ( 𝜑 → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) ) |
10 |
|
ssid |
⊢ ℂ ⊆ ℂ |
11 |
|
eqid |
⊢ ( 𝐽 ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 ) |
12 |
5
|
toponrestid |
⊢ 𝐽 = ( 𝐽 ↾t ℂ ) |
13 |
1 11 12
|
cncfcn |
⊢ ( ( 𝑋 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋 –cn→ ℂ ) = ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) ) |
14 |
7 10 13
|
sylancl |
⊢ ( 𝜑 → ( 𝑋 –cn→ ℂ ) = ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) ) |
15 |
3 14
|
eleqtrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) ) |
16 |
4 14
|
eleqtrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) ) |
17 |
9 15 16 2
|
cnmpt12f |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) ) |
18 |
17 14
|
eleqtrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) ) |