Theorem xnegex

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

	Ref	Expression
Assertion	xnegex	⊢ -𝑒 𝐴 ∈ V

Proof

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