Theorem ioof 13457

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.)

Assertion

Ref	Expression
ioof	⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ

Proof of Theorem ioof

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iooval 13381	. . . 4 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥(,)𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2		ioossre 13418	. . . . 5 ⊢ (𝑥(,)𝑦) ⊆ ℝ
3		ovex 7453	. . . . . 6 ⊢ (𝑥(,)𝑦) ∈ V
4	3	elpw 4607	. . . . 5 ⊢ ((𝑥(,)𝑦) ∈ 𝒫 ℝ ↔ (𝑥(,)𝑦) ⊆ ℝ)
5	2, 4	mpbir 230	. . . 4 ⊢ (𝑥(,)𝑦) ∈ 𝒫 ℝ
6	1, 5	eqeltrrdi 2838	. . 3 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} ∈ 𝒫 ℝ)
7	6	rgen2 3194	. 2 ⊢ ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} ∈ 𝒫 ℝ
8		df-ioo 13361	. . 3 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
9	8	fmpo 8072	. 2 ⊢ (∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} ∈ 𝒫 ℝ ↔ (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
10	7, 9	mpbi 229	1 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ

Syntax hints:   ∧ wa 395   ∈ wcel 2099  ∀wral 3058  {crab 3429   ⊆ wss 3947  𝒫 cpw 4603   class class class wbr 5148   × cxp 5676  ⟶wf 6544  (class class class)co 7420  ℝcr 11138  ℝ^*cxr 11278   < clt 11279  (,)cioo 13357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-resscn 11196  ax-pre-lttri 11213  ax-pre-lttrn 11214

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 7993  df-2nd 7994  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-ioo 13361

This theorem is referenced by:  unirnioo  13459  dfioo2  13460  ioorebas  13461  qtopbaslem  24688  retopbas  24690  qdensere  24699  blssioo  24724  tgioo  24725  tgqioo  24729  re2ndc  24730  xrtgioo  24735  xrge0tsms  24763  bndth  24897  ovolfioo  25409  ovollb  25421  ovolicc2  25464  ovolfs2  25513  ioorf  25515  ioorinv  25518  ioorcl  25519  uniiccdif  25520  uniioovol  25521  uniiccvol  25522  uniioombllem2  25525  uniioombllem3a  25526  uniioombllem3  25527  uniioombllem4  25528  uniioombllem5  25529  uniioombl  25531  opnmblALT  25545  mbfdm  25568  mbfima  25572  mbfid  25577  ismbfd  25581  mbfimaopnlem  25597  i1fd  25623  xrge0tsmsd  32784  iccllysconn  34860  rellysconn  34861  relowlssretop  36842  relowlpssretop  36843  ftc1anc  37174  ftc2nc  37175  ioofun  44936  islptre  45007  volioof  45375  fvvolioof  45377  ovolval3  46035  ovolval4lem1  46037  ovolval5lem2  46041  ovolval5lem3  46042