Metamath Proof Explorer


Theorem elxr

Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion elxr A * A A = +∞ A = −∞

Proof

Step Hyp Ref Expression
1 df-xr * = +∞ −∞
2 1 eleq2i A * A +∞ −∞
3 elun A +∞ −∞ A A +∞ −∞
4 pnfex +∞ V
5 mnfxr −∞ *
6 5 elexi −∞ V
7 4 6 elpr2 A +∞ −∞ A = +∞ A = −∞
8 7 orbi2i A A +∞ −∞ A A = +∞ A = −∞
9 3orass A A = +∞ A = −∞ A A = +∞ A = −∞
10 8 9 bitr4i A A +∞ −∞ A A = +∞ A = −∞
11 2 3 10 3bitri A * A A = +∞ A = −∞