mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8102

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 8083	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8099	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4217	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2269	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3730	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3332	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8084	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2272	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2167 Vcvv 2763 ∪ cun 3155 𝒫 cpw 3606 {cpr 3624 ℝcr 7897 +∞cpnf 8077 -∞cmnf 8078 ℝ^*cxr 8079

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 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-un 4469 ax-cnex 7989

This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1475 df-sb 1777 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-rex 2481 df-v 2765 df-un 3161 df-in 3163 df-ss 3170 df-pw 3608 df-sn 3629 df-pr 3630 df-uni 3841 df-pnf 8082 df-mnf 8083 df-xr 8084

This theorem is referenced by: elxr 9870 xrltnr 9873 mnflt 9877 mnfltpnf 9879 nltmnf 9882 mnfle 9886 xrltnsym 9887 xrlttri3 9891 ngtmnft 9911 xrrebnd 9913 xrre2 9915 xrre3 9916 ge0gtmnf 9917 xnegcl 9926 xltnegi 9929 xaddf 9938 xaddval 9939 xaddmnf1 9942 xaddmnf2 9943 pnfaddmnf 9944 mnfaddpnf 9945 xrex 9950 xltadd1 9970 xlt2add 9974 xsubge0 9975 xposdif 9976 xleaddadd 9981 elioc2 10030 elico2 10031 elicc2 10032 ioomax 10042 iccmax 10043 elioomnf 10062 unirnioo 10067 xrmaxadd 11445 reopnap 14868 blssioo 14875 tgioo 14876

W3C validator