elxr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elxr		Structured version Visualization version GIF version

Theorem elxr 12499

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

**Assertion**
Ref	Expression
elxr	⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

**Proof of Theorem elxr**
Step	Hyp	Ref	Expression
1		df-xr 10668	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2881	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4076	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 10683	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 10687	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3460	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4550	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 910	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1087	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 281	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 300	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 209 ∨ wo 844 ∨ w3o 1083 = wceq 1538 ∈ wcel 2111 ∪ cun 3879 {cpr 4527 ℝcr 10525 +∞cpnf 10661 -∞cmnf 10662 ℝ^*cxr 10663

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-pow 5231 ax-un 7441 ax-cnex 10582

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-pw 4499 df-sn 4526 df-pr 4528 df-uni 4801 df-pnf 10666 df-mnf 10667 df-xr 10668

This theorem is referenced by: xrnemnf 12500 xrnepnf 12501 xrltnr 12502 xrltnsym 12518 xrlttri 12520 xrlttr 12521 xrrebnd 12549 qbtwnxr 12581 xnegcl 12594 xnegneg 12595 xltnegi 12597 xaddf 12605 xnegid 12619 xaddcom 12621 xaddid1 12622 xnegdi 12629 xleadd1a 12634 xlt2add 12641 xsubge0 12642 xmullem 12645 xmulid1 12660 xmulgt0 12664 xmulasslem3 12667 xlemul1a 12669 xadddilem 12675 xadddi2 12678 xrsupsslem 12688 xrinfmsslem 12689 xrub 12693 reltxrnmnf 12723 isxmet2d 22934 blssioo 23400 ioombl1 24166 ismbf2d 24244 itg2seq 24346 xaddeq0 30503 iooelexlt 34779 relowlssretop 34780 iccpartiltu 43939 iccpartigtl 43940