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

Metamath Proof Explorer

Theorem xnegex

Description: A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xnegex ⊢ − A ∈ V

Proof

Step Hyp Ref Expression
1 df-xneg ⊢ − A = if A = +∞ −∞ if A = −∞ +∞ − A
2 mnfxr ⊢ −∞ ∈ ℝ *
3 2 elexi ⊢ −∞ ∈ V
4 pnfex ⊢ +∞ ∈ V
5 negex ⊢ − A ∈ V
6 4 5 ifex ⊢ if A = −∞ +∞ − A ∈ V
7 3 6 ifex ⊢ if A = +∞ −∞ if A = −∞ +∞ − A ∈ V
8 1 7 eqeltri ⊢ − A ∈ V