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 12505

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 10673	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2904	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4125	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 10688	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 10692	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3514	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4585	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 909	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1086	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 280	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 299	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∨ wo 843 ∨ w3o 1082 = wceq 1533 ∈ wcel 2110 ∪ cun 3934 {cpr 4563 ℝcr 10530 +∞cpnf 10666 -∞cmnf 10667 ℝ^*cxr 10668

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-pow 5259 ax-un 7455 ax-cnex 10587

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-v 3497 df-un 3941 df-in 3943 df-ss 3952 df-pw 4541 df-sn 4562 df-pr 4564 df-uni 4833 df-pnf 10671 df-mnf 10672 df-xr 10673

This theorem is referenced by: xrnemnf 12506 xrnepnf 12507 xrltnr 12508 xrltnsym 12524 xrlttri 12526 xrlttr 12527 xrrebnd 12555 qbtwnxr 12587 xnegcl 12600 xnegneg 12601 xltnegi 12603 xaddf 12611 xnegid 12625 xaddcom 12627 xaddid1 12628 xnegdi 12635 xleadd1a 12640 xlt2add 12647 xsubge0 12648 xmullem 12651 xmulid1 12666 xmulgt0 12670 xmulasslem3 12673 xlemul1a 12675 xadddilem 12681 xadddi2 12684 xrsupsslem 12694 xrinfmsslem 12695 xrub 12699 reltxrnmnf 12729 isxmet2d 22931 blssioo 23397 ioombl1 24157 ismbf2d 24235 itg2seq 24337 xaddeq0 30471 iooelexlt 34637 relowlssretop 34638 iccpartiltu 43575 iccpartigtl 43576