Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ioof | Structured version Visualization version GIF version |
Description: The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Ref | Expression |
---|---|
ioof | ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iooval 13153 | . . . 4 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥(,)𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | |
2 | ioossre 13190 | . . . . 5 ⊢ (𝑥(,)𝑦) ⊆ ℝ | |
3 | ovex 7340 | . . . . . 6 ⊢ (𝑥(,)𝑦) ∈ V | |
4 | 3 | elpw 4543 | . . . . 5 ⊢ ((𝑥(,)𝑦) ∈ 𝒫 ℝ ↔ (𝑥(,)𝑦) ⊆ ℝ) |
5 | 2, 4 | mpbir 230 | . . . 4 ⊢ (𝑥(,)𝑦) ∈ 𝒫 ℝ |
6 | 1, 5 | eqeltrrdi 2846 | . . 3 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} ∈ 𝒫 ℝ) |
7 | 6 | rgen2 3191 | . 2 ⊢ ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} ∈ 𝒫 ℝ |
8 | df-ioo 13133 | . . 3 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | |
9 | 8 | fmpo 7940 | . 2 ⊢ (∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} ∈ 𝒫 ℝ ↔ (,):(ℝ* × ℝ*)⟶𝒫 ℝ) |
10 | 7, 9 | mpbi 229 | 1 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 ∈ wcel 2104 ∀wral 3062 {crab 3303 ⊆ wss 3892 𝒫 cpw 4539 class class class wbr 5081 × cxp 5598 ⟶wf 6454 (class class class)co 7307 ℝcr 10920 ℝ*cxr 11058 < clt 11059 (,)cioo 13129 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-cnex 10977 ax-resscn 10978 ax-pre-lttri 10995 ax-pre-lttrn 10996 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3306 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-iun 4933 df-br 5082 df-opab 5144 df-mpt 5165 df-id 5500 df-po 5514 df-so 5515 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-ov 7310 df-oprab 7311 df-mpo 7312 df-1st 7863 df-2nd 7864 df-er 8529 df-en 8765 df-dom 8766 df-sdom 8767 df-pnf 11061 df-mnf 11062 df-xr 11063 df-ltxr 11064 df-le 11065 df-ioo 13133 |
This theorem is referenced by: unirnioo 13231 dfioo2 13232 ioorebas 13233 qtopbaslem 23971 retopbas 23973 qdensere 23982 blssioo 24007 tgioo 24008 tgqioo 24012 re2ndc 24013 xrtgioo 24018 xrge0tsms 24046 bndth 24170 ovolfioo 24680 ovollb 24692 ovolicc2 24735 ovolfs2 24784 ioorf 24786 ioorinv 24789 ioorcl 24790 uniiccdif 24791 uniioovol 24792 uniiccvol 24793 uniioombllem2 24796 uniioombllem3a 24797 uniioombllem3 24798 uniioombllem4 24799 uniioombllem5 24800 uniioombl 24802 opnmblALT 24816 mbfdm 24839 mbfima 24843 mbfid 24848 ismbfd 24852 mbfimaopnlem 24868 i1fd 24894 xrge0tsmsd 31366 iccllysconn 33261 rellysconn 33262 relowlssretop 35582 relowlpssretop 35583 ftc1anc 35906 ftc2nc 35907 ioofun 43318 islptre 43389 volioof 43757 fvvolioof 43759 ovolval3 44415 ovolval4lem1 44417 ovolval5lem2 44421 ovolval5lem3 44422 |
Copyright terms: Public domain | W3C validator |