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 12852

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 11013	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2830	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4083	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11028	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11032	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3451	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4586	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 910	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1089	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 277	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 297	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∨ wo 844 ∨ w3o 1085 = wceq 1539 ∈ wcel 2106 ∪ cun 3885 {cpr 4563 ℝcr 10870 +∞cpnf 11006 -∞cmnf 11007 ℝ^*cxr 11008

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-pow 5288 ax-un 7588 ax-cnex 10927

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-un 3892 df-in 3894 df-ss 3904 df-pw 4535 df-sn 4562 df-pr 4564 df-uni 4840 df-pnf 11011 df-mnf 11012 df-xr 11013

This theorem is referenced by: xrnemnf 12853 xrnepnf 12854 xrltnr 12855 xrltnsym 12871 xrlttri 12873 xrlttr 12874 xrrebnd 12902 qbtwnxr 12934 xnegcl 12947 xnegneg 12948 xltnegi 12950 xaddf 12958 xnegid 12972 xaddcom 12974 xaddid1 12975 xnegdi 12982 xleadd1a 12987 xlt2add 12994 xsubge0 12995 xmullem 12998 xmulid1 13013 xmulgt0 13017 xmulasslem3 13020 xlemul1a 13022 xadddilem 13028 xadddi2 13031 xrsupsslem 13041 xrinfmsslem 13042 xrub 13046 reltxrnmnf 13076 isxmet2d 23480 blssioo 23958 ioombl1 24726 ismbf2d 24804 itg2seq 24907 xaddeq0 31076 iooelexlt 35533 relowlssretop 35534 iccpartiltu 44874 iccpartigtl 44875