mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8203

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 8184	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8200	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4267	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2302	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3773	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3372	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8185	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2305	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2200 Vcvv 2799 ∪ cun 3195 𝒫 cpw 3649 {cpr 3667 ℝcr 7998 +∞cpnf 8178 -∞cmnf 8179 ℝ^*cxr 8180

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 4202 ax-pow 4258 ax-un 4524 ax-cnex 8090

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 2801 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-uni 3889 df-pnf 8183 df-mnf 8184 df-xr 8185

This theorem is referenced by: elxr 9972 xrltnr 9975 mnflt 9979 mnfltpnf 9981 nltmnf 9984 mnfle 9988 xrltnsym 9989 xrlttri3 9993 ngtmnft 10013 xrrebnd 10015 xrre2 10017 xrre3 10018 ge0gtmnf 10019 xnegcl 10028 xltnegi 10031 xaddf 10040 xaddval 10041 xaddmnf1 10044 xaddmnf2 10045 pnfaddmnf 10046 mnfaddpnf 10047 xrex 10052 xltadd1 10072 xlt2add 10076 xsubge0 10077 xposdif 10078 xleaddadd 10083 elioc2 10132 elico2 10133 elicc2 10134 ioomax 10144 iccmax 10145 elioomnf 10164 unirnioo 10169 xrmaxadd 11772 reopnap 15220 blssioo 15227 tgioo 15228

W3C validator