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 ⊢ F = x ∈ A ⟼ − x
Assertion negcncfOLD ⊢ A ⊆ ℂ → F : A ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 negcncfOLD.1 ⊢ F = x ∈ A ⟼ − x
2 ssel2 ⊢ A ⊆ ℂ ∧ x ∈ A → x ∈ ℂ
3 2 mulm1d ⊢ A ⊆ ℂ ∧ x ∈ A → -1 ⁢ x = − x
4 3 mpteq2dva ⊢ A ⊆ ℂ → x ∈ A ⟼ -1 ⁢ x = x ∈ A ⟼ − x
5 4 1 eqtr4di ⊢ A ⊆ ℂ → x ∈ A ⟼ -1 ⁢ x = F
6 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
7 6 mulcn ⊢ × ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
8 7 a1i ⊢ A ⊆ ℂ → × ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
9 neg1cn ⊢ − 1 ∈ ℂ
10 ssid ⊢ ℂ ⊆ ℂ
11 cncfmptc ⊢ − 1 ∈ ℂ ∧ A ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ A ⟼ − 1 : A ⟶cn ℂ
12 9 10 11 mp3an13 ⊢ A ⊆ ℂ → x ∈ A ⟼ − 1 : A ⟶cn ℂ
13 cncfmptid ⊢ A ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ A ⟼ x : A ⟶cn ℂ
14 10 13 mpan2 ⊢ A ⊆ ℂ → x ∈ A ⟼ x : A ⟶cn ℂ
15 6 8 12 14 cncfmpt2f ⊢ A ⊆ ℂ → x ∈ A ⟼ -1 ⁢ x : A ⟶cn ℂ
16 5 15 eqeltrrd ⊢ A ⊆ ℂ → F : A ⟶cn ℂ