elioomnf - Metamath Proof Explorer

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

Theorem elioomnf 13346

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

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

**Proof of Theorem elioomnf**
Step	Hyp	Ref	Expression
1		mnfxr 11176	. . 3 ⊢ -∞ ∈ ℝ^*
2		elioo2 13288	. . 3 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ -∞ < 𝐵 ∧ 𝐵 < 𝐴)))
3	1, 2	mpan 690	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ -∞ < 𝐵 ∧ 𝐵 < 𝐴)))
4		an32 646	. . 3 ⊢ (((𝐵 ∈ ℝ ∧ -∞ < 𝐵) ∧ 𝐵 < 𝐴) ↔ ((𝐵 ∈ ℝ ∧ 𝐵 < 𝐴) ∧ -∞ < 𝐵))
5		df-3an 1088	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ -∞ < 𝐵 ∧ 𝐵 < 𝐴) ↔ ((𝐵 ∈ ℝ ∧ -∞ < 𝐵) ∧ 𝐵 < 𝐴))
6		mnflt 13024	. . . . 5 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
7	6	adantr 480	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 < 𝐴) → -∞ < 𝐵)
8	7	pm4.71i 559	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 < 𝐴) ↔ ((𝐵 ∈ ℝ ∧ 𝐵 < 𝐴) ∧ -∞ < 𝐵))
9	4, 5, 8	3bitr4i 303	. 2 ⊢ ((𝐵 ∈ ℝ ∧ -∞ < 𝐵 ∧ 𝐵 < 𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴))
10	3, 9	bitrdi 287	1 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2113 class class class wbr 5093 (class class class)co 7352 ℝcr 11012 -∞cmnf 11151 ℝ^*cxr 11152 < clt 11153 (,)cioo 13247

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-pre-lttri 11087 ax-pre-lttrn 11088

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-id 5514 df-po 5527 df-so 5528 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-ov 7355 df-oprab 7356 df-mpo 7357 df-1st 7927 df-2nd 7928 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-ioo 13251

This theorem is referenced by: bndth 24885 mbfmulc2lem 25576 mbfposr 25581 ismbf3d 25583 mbfi1fseqlem4 25647 itg2monolem1 25679 dvne0 25944 mbfposadd 37727 itg2addnclem2 37732 iblabsnclem 37743 ftc1anclem1 37753 ftc1anclem6 37758 redvmptabs 42478 rfcnpre2 45152 i0oii 49044

W3C validator