Theorem ngtmnft

Description: An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006)

	Ref	Expression
Assertion	ngtmnft	|- ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )

Proof

Step	Hyp	Ref	Expression
1		mnfxr	|- -oo e. RR*
2		xrltnr	|- ( -oo e. RR* -> -. -oo < -oo )
3	1 2	ax-mp	|- -. -oo < -oo
4		breq2	|- ( A = -oo -> ( -oo < A <-> -oo < -oo ) )
5	3 4	mtbiri	|- ( A = -oo -> -. -oo < A )
6		mnfle	|- ( A e. RR* -> -oo <_ A )
7		xrleloe	|- ( ( -oo e. RR* /\ A e. RR* ) -> ( -oo <_ A <-> ( -oo < A \/ -oo = A ) ) )
8	1 7	mpan	|- ( A e. RR* -> ( -oo <_ A <-> ( -oo < A \/ -oo = A ) ) )
9	6 8	mpbid	|- ( A e. RR* -> ( -oo < A \/ -oo = A ) )
10	9	ord	|- ( A e. RR* -> ( -. -oo < A -> -oo = A ) )
11		eqcom	|- ( -oo = A <-> A = -oo )
12	10 11	imbitrdi	|- ( A e. RR* -> ( -. -oo < A -> A = -oo ) )
13	5 12	impbid2	|- ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )