elioopnf - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elioopnf		Structured version Visualization version GIF version

Theorem elioopnf 13380

Description: Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)

**Assertion**
Ref	Expression
elioopnf	⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)))

**Proof of Theorem elioopnf**
Step	Hyp	Ref	Expression
1		pnfxr 11204	. . 3 ⊢ +∞ ∈ ℝ^*
2		elioo2 13323	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞)))
3	1, 2	mpan2 691	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞)))
4		df-3an 1088	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝐵 < +∞))
5		ltpnf 13056	. . . . 5 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
6	5	adantr 480	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 < +∞)
7	6	pm4.71i 559	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝐵 < +∞))
8	4, 7	bitr4i 278	. 2 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
9	3, 8	bitrdi 287	1 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2109 class class class wbr 5102 (class class class)co 7369 ℝcr 11043 +∞cpnf 11181 ℝ^*cxr 11183 < clt 11184 (,)cioo 13282

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-pre-lttri 11118 ax-pre-lttrn 11119

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-po 5539 df-so 5540 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-ov 7372 df-oprab 7373 df-mpo 7374 df-1st 7947 df-2nd 7948 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-ioo 13286

This theorem is referenced by: mbfmulc2lem 25581 mbfposr 25586 ismbf3d 25588 mbfaddlem 25594 mbfsup 25598 itg2gt0 25694 itg2cnlem1 25695 itg2cnlem2 25696 lhop2 25953 dvfsumlem2 25966 dvfsumlem2OLD 25967 dvfsumlem3 25968 dvfsumrlimge0 25970 dvfsumrlim 25971 dvfsumrlim2 25972 pntpbnd1a 27529 pntpbnd2 27531 pntibndlem2 27535 pntibndlem3 27536 pntlemi 27548 pntlemo 27551 relowlssretop 37344 itg2addnclem2 37659 iblabsnclem 37670 ftc1anclem1 37680 ftc1anclem6 37685 rfcnpre1 45006 regt1loggt0 48518 rege1logbrege0 48540 rege1logbzge0 48541 io1ii 48902

W3C validator