Theorem xnegex

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

	Ref	Expression
Assertion	xnegex	|- -e A e. _V

Proof

Step	Hyp	Ref	Expression
1		df-xneg	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
2		mnfxr	|- -oo e. RR*
3	2	elexi	|- -oo e. _V
4		pnfex	|- +oo e. _V
5		negex	|- -u A e. _V
6	4 5	ifex	|- if ( A = -oo , +oo , -u A ) e. _V
7	3 6	ifex	|- if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) e. _V
8	1 7	eqeltri	|- -e A e. _V