This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem negcncfOLD

Description: Obsolete version of negcncf as of 9-Apr-2025. (Contributed by Mario Carneiro, 30-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis negcncfOLD.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 )
Assertion negcncfOLD ( 𝐴 ⊆ ℂ → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 negcncfOLD.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→ ℂ ) )