mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8229

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 8210	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8226	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4271	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2302	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3776	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3373	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8211	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2305	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2200 Vcvv 2800 ∪ cun 3196 𝒫 cpw 3650 {cpr 3668 ℝcr 8024 +∞cpnf 8204 -∞cmnf 8205 ℝ^*cxr 8206

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 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4205 ax-pow 4262 ax-un 4528 ax-cnex 8116

This theorem depends on definitions: df-bi 117 df-tru 1398 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-rex 2514 df-v 2802 df-un 3202 df-in 3204 df-ss 3211 df-pw 3652 df-sn 3673 df-pr 3674 df-uni 3892 df-pnf 8209 df-mnf 8210 df-xr 8211

This theorem is referenced by: elxr 10004 xrltnr 10007 mnflt 10011 mnfltpnf 10013 nltmnf 10016 mnfle 10020 xrltnsym 10021 xrlttri3 10025 ngtmnft 10045 xrrebnd 10047 xrre2 10049 xrre3 10050 ge0gtmnf 10051 xnegcl 10060 xltnegi 10063 xaddf 10072 xaddval 10073 xaddmnf1 10076 xaddmnf2 10077 pnfaddmnf 10078 mnfaddpnf 10079 xrex 10084 xltadd1 10104 xlt2add 10108 xsubge0 10109 xposdif 10110 xleaddadd 10115 elioc2 10164 elico2 10165 elicc2 10166 ioomax 10176 iccmax 10177 elioomnf 10196 unirnioo 10201 xrmaxadd 11815 reopnap 15263 blssioo 15270 tgioo 15271

W3C validator