Theorem i1ff 25647

Description: A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.)

Assertion

Ref	Expression
i1ff	⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ)

Proof of Theorem i1ff

Step	Hyp	Ref	Expression
1		isi1f 25645	. . 3 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
2	1	simprbi 496	. 2 ⊢ (𝐹 ∈ dom ∫1 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
3	2	simp1d 1142	1 ⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ)

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2107   ∖ cdif 3928  {csn 4606  ^◡ccnv 5664  dom cdm 5665  ran crn 5666   “ cima 5668  ⟶wf 6537  ‘cfv 6541  Fincfn 8967  ℝcr 11136  0cc0 11137  volcvol 25434  MblFncmbf 25585  ∫₁citg1 25586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-sum 15705  df-itg1 25591

This theorem is referenced by:  i1fima  25649  i1fima2  25650  i1f0rn  25653  itg1val2  25655  itg1cl  25656  itg1ge0  25657  i1faddlem  25664  i1fmullem  25665  i1fadd  25666  i1fmul  25667  itg1addlem4  25670  itg1addlem5  25671  i1fmulclem  25673  i1fmulc  25674  itg1mulc  25675  i1fres  25676  i1fpos  25677  i1fposd  25678  i1fsub  25679  itg1sub  25680  itg10a  25681  itg1ge0a  25682  itg1lea  25683  itg1le  25684  itg1climres  25685  mbfi1fseqlem5  25690  mbfi1fseqlem6  25691  mbfi1flimlem  25693  mbfmullem2  25695  itg2itg1  25707  itg20  25708  itg2le  25710  itg2seq  25713  itg2uba  25714  itg2lea  25715  itg2mulclem  25717  itg2splitlem  25719  itg2split  25720  itg2monolem1  25721  itg2i1fseqle  25725  itg2i1fseq  25726  itg2addlem  25729  i1fibl  25779  itgitg1  25780  itg2addnclem  37637  itg2addnclem2  37638  itg2addnclem3  37639  itg2addnc  37640  ftc1anclem3  37661  ftc1anclem4  37662  ftc1anclem5  37663  ftc1anclem6  37664  ftc1anclem7  37665  ftc1anclem8  37666  ftc1anc  37667