elioo4g - Metamath Proof Explorer

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

Theorem elioo4g 13433

Description: Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)

**Assertion**
Ref	Expression
elioo4g	⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

**Proof of Theorem elioo4g**
Step	Hyp	Ref	Expression
1		eliooxr 13431	. . . . 5 ⊢ (𝐶 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
2		elioore 13402	. . . . 5 ⊢ (𝐶 ∈ (𝐴(,)𝐵) → 𝐶 ∈ ℝ)
3	1, 2	jca 520	. . . 4 ⊢ (𝐶 ∈ (𝐴(,)𝐵) → ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ))
4		df-3an 1103	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ) ↔ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ))
5	3, 4	sylibr 237	. . 3 ⊢ (𝐶 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ))
6		eliooord 13432	. . 3 ⊢ (𝐶 ∈ (𝐴(,)𝐵) → (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
7	5, 6	jca 520	. 2 ⊢ (𝐶 ∈ (𝐴(,)𝐵) → ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8		rexr 11255	. . . . 5 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
9	8	3anim3i 1170	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*))
10	9	anim1i 626	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)) → ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
11		elioo3g 13401	. . 3 ⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
12	10, 11	sylibr 237	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 ∈ (𝐴(,)𝐵))
13	7, 12	impbii 212	1 ⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 209 ∧ wa 400 ∧ w3a 1101 ∈ wcel 2149 class class class wbr 5113 (class class class)co 7411 ℝcr 11099 ℝ^*cxr 11242 < clt 11243 (,)cioo 13372

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-pre-lttri 11174 ax-pre-lttrn 11175

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-po 5570 df-so 5571 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7986 df-2nd 7987 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-ioo 13376

This theorem is referenced by: cncfiooicclem1 46533 fourierdlem89 46835 fourierdlem90 46836 fourierdlem91 46837 fourierdlem100 46846

W3C validator