mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 7822

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 7803	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 7819	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4107	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2212	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3630	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3244	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 7804	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2215	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 1480 Vcvv 2686 ∪ cun 3069 𝒫 cpw 3510 {cpr 3528 ℝcr 7619 +∞cpnf 7797 -∞cmnf 7798 ℝ^*cxr 7799

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-un 4355 ax-cnex 7711

This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-uni 3737 df-pnf 7802 df-mnf 7803 df-xr 7804

This theorem is referenced by: elxr 9563 xrltnr 9566 mnflt 9569 mnfltpnf 9571 nltmnf 9574 mnfle 9578 xrltnsym 9579 xrlttri3 9583 ngtmnft 9600 xrrebnd 9602 xrre2 9604 xrre3 9605 ge0gtmnf 9606 xnegcl 9615 xltnegi 9618 xaddf 9627 xaddval 9628 xaddmnf1 9631 xaddmnf2 9632 pnfaddmnf 9633 mnfaddpnf 9634 xrex 9639 xltadd1 9659 xlt2add 9663 xsubge0 9664 xposdif 9665 xleaddadd 9670 elioc2 9719 elico2 9720 elicc2 9721 ioomax 9731 iccmax 9732 elioomnf 9751 unirnioo 9756 xrmaxadd 11030 reopnap 12707 blssioo 12714 tgioo 12715

W3C validator