mnfxr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mnfxr		GIF version

Theorem mnfxr 8236

Description: Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)

**Assertion**
Ref	Expression
mnfxr	⊢ -∞ ∈ ℝ^*

**Proof of Theorem mnfxr**
Step	Hyp	Ref	Expression
1		df-mnf 8217	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8233	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4273	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2304	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3778	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3375	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8218	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2307	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2202 Vcvv 2802 ∪ cun 3198 𝒫 cpw 3652 {cpr 3670 ℝcr 8031 +∞cpnf 8211 -∞cmnf 8212 ℝ^*cxr 8213

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-un 4530 ax-cnex 8123

This theorem depends on definitions: df-bi 117 df-tru 1400 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-rex 2516 df-v 2804 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-uni 3894 df-pnf 8216 df-mnf 8217 df-xr 8218

This theorem is referenced by: elxr 10011 xrltnr 10014 mnflt 10018 mnfltpnf 10020 nltmnf 10023 mnfle 10027 xrltnsym 10028 xrlttri3 10032 ngtmnft 10052 xrrebnd 10054 xrre2 10056 xrre3 10057 ge0gtmnf 10058 xnegcl 10067 xltnegi 10070 xaddf 10079 xaddval 10080 xaddmnf1 10083 xaddmnf2 10084 pnfaddmnf 10085 mnfaddpnf 10086 xrex 10091 xltadd1 10111 xlt2add 10115 xsubge0 10116 xposdif 10117 xleaddadd 10122 elioc2 10171 elico2 10172 elicc2 10173 ioomax 10183 iccmax 10184 elioomnf 10203 unirnioo 10208 xrmaxadd 11823 reopnap 15273 blssioo 15280 tgioo 15281

W3C validator