unirnioo - Metamath Proof Explorer

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

Theorem unirnioo 12215

Description: The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)

**Assertion**
Ref	Expression
unirnioo	⊢ ℝ = ∪ ran (,)

**Proof of Theorem unirnioo**
Step	Hyp	Ref	Expression
1		ioomax 12190	. . . 4 ⊢ (-∞(,)+∞) = ℝ
2		ioof 12213	. . . . . 6 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
3		ffn 6002	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
4	2, 3	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
5		mnfxr 10040	. . . . 5 ⊢ -∞ ∈ ℝ^*
6		pnfxr 10036	. . . . 5 ⊢ +∞ ∈ ℝ^*
7		fnovrn 6762	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ -∞ ∈ ℝ^ ∧ +∞ ∈ ℝ^*) → (-∞(,)+∞) ∈ ran (,))
8	4, 5, 6, 7	mp3an 1421	. . . 4 ⊢ (-∞(,)+∞) ∈ ran (,)
9	1, 8	eqeltrri 2695	. . 3 ⊢ ℝ ∈ ran (,)
10		elssuni 4433	. . 3 ⊢ (ℝ ∈ ran (,) → ℝ ⊆ ∪ ran (,))
11	9, 10	ax-mp 5	. 2 ⊢ ℝ ⊆ ∪ ran (,)
12		frn 6010	. . . 4 ⊢ ((,):(ℝ^* × ℝ^*)⟶𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ)
13	2, 12	ax-mp 5	. . 3 ⊢ ran (,) ⊆ 𝒫 ℝ
14		sspwuni 4577	. . 3 ⊢ (ran (,) ⊆ 𝒫 ℝ ↔ ∪ ran (,) ⊆ ℝ)
15	13, 14	mpbi 220	. 2 ⊢ ∪ ran (,) ⊆ ℝ
16	11, 15	eqssi 3599	1 ⊢ ℝ = ∪ ran (,)

Colors of variables: wff setvar class

Syntax hints: = wceq 1480 ∈ wcel 1987 ⊆ wss 3555 𝒫 cpw 4130 ∪ cuni 4402 × cxp 5072 ran crn 5075 Fn wfn 5842 ⟶wf 5843 (class class class)co 6604 ℝcr 9879 +∞cpnf 10015 -∞cmnf 10016 ℝ^*cxr 10017 (,)cioo 12117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-cnex 9936 ax-resscn 9937 ax-pre-lttri 9954 ax-pre-lttrn 9955

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-op 4155 df-uni 4403 df-iun 4487 df-br 4614 df-opab 4674 df-mpt 4675 df-id 4989 df-po 4995 df-so 4996 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-1st 7113 df-2nd 7114 df-er 7687 df-en 7900 df-dom 7901 df-sdom 7902 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-ioo 12121

This theorem is referenced by: pnfnei 20934 mnfnei 20935 uniretop 22476 tgioo 22507 xrtgioo 22517 bndth 22665 relowlssretop 32843 relowlpssretop 32844 mblfinlem3 33080 mblfinlem4 33081 ismblfin 33082

W3C validator