Theorem xrgepnfd

Description: An extended real greater than or equal to +oo is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	xrgepnfd.1	|- ( ph -> A e. RR* )
	xrgepnfd.2	|- ( ph -> +oo <_ A )
Assertion	xrgepnfd	|- ( ph -> A = +oo )

Proof

Step	Hyp	Ref	Expression
1		xrgepnfd.1	|- ( ph -> A e. RR* )
2		xrgepnfd.2	|- ( ph -> +oo <_ A )
3		pnfxr	|- +oo e. RR*
4	3	a1i	|- ( ph -> +oo e. RR* )
5		pnfge	|- ( A e. RR* -> A <_ +oo )
6	1 5	syl	|- ( ph -> A <_ +oo )
7	1 4 6 2	xrletrid	|- ( ph -> A = +oo )