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	$$⊢\phi \to A\in {ℝ}^{*}$$
	xrgepnfd.2	$$⊢\phi \to \mathrm{+\infty }\le A$$
Assertion	xrgepnfd	$$⊢\phi \to A=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		xrgepnfd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrgepnfd.2	$$⊢\phi \to \mathrm{+\infty }\le A$$
3		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
4	3	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
5		pnfge	$$⊢A\in {ℝ}^{*}\to A\le \mathrm{+\infty }$$
6	1 5	syl	$$⊢\phi \to A\le \mathrm{+\infty }$$
7	1 4 6 2	xrletrid	$$⊢\phi \to A=\mathrm{+\infty }$$