Step |
Hyp |
Ref |
Expression |
1 |
|
negcncf.1 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 ) |
2 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℂ ) |
3 |
2
|
mulm1d |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( - 1 · 𝑥 ) = - 𝑥 ) |
4 |
3
|
mpteq2dva |
⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ ( - 1 · 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 ) ) |
5 |
4 1
|
eqtr4di |
⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ ( - 1 · 𝑥 ) ) = 𝐹 ) |
6 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
7 |
6
|
mulcn |
⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
8 |
7
|
a1i |
⊢ ( 𝐴 ⊆ ℂ → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
9 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
10 |
|
ssid |
⊢ ℂ ⊆ ℂ |
11 |
|
cncfmptc |
⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ - 1 ) ∈ ( 𝐴 –cn→ ℂ ) ) |
12 |
9 10 11
|
mp3an13 |
⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ - 1 ) ∈ ( 𝐴 –cn→ ℂ ) ) |
13 |
|
cncfmptid |
⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) ) |
14 |
10 13
|
mpan2 |
⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) ) |
15 |
6 8 12 14
|
cncfmpt2f |
⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ ( - 1 · 𝑥 ) ) ∈ ( 𝐴 –cn→ ℂ ) ) |
16 |
5 15
|
eqeltrrd |
⊢ ( 𝐴 ⊆ ℂ → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) |