Theorem i1ff 25653

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 25651	. . 3 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
2	1	simprbi 497	. 2 ⊢ (𝐹 ∈ dom ∫1 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
3	2	simp1d 1143	1 ⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ)

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114   ∖ cdif 3887  {csn 4568  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   “ cima 5627  ⟶wf 6488  ‘cfv 6492  Fincfn 8886  ℝcr 11028  0cc0 11029  volcvol 25440  MblFncmbf 25591  ∫₁citg1 25592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-sum 15640  df-itg1 25597

This theorem is referenced by:  i1fima  25655  i1fima2  25656  i1f0rn  25659  itg1val2  25661  itg1cl  25662  itg1ge0  25663  i1faddlem  25670  i1fmullem  25671  i1fadd  25672  i1fmul  25673  itg1addlem4  25676  itg1addlem5  25677  i1fmulclem  25679  i1fmulc  25680  itg1mulc  25681  i1fres  25682  i1fpos  25683  i1fposd  25684  i1fsub  25685  itg1sub  25686  itg10a  25687  itg1ge0a  25688  itg1lea  25689  itg1le  25690  itg1climres  25691  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  mbfi1flimlem  25699  mbfmullem2  25701  itg2itg1  25713  itg20  25714  itg2le  25716  itg2seq  25719  itg2uba  25720  itg2lea  25721  itg2mulclem  25723  itg2splitlem  25725  itg2split  25726  itg2monolem1  25727  itg2i1fseqle  25731  itg2i1fseq  25732  itg2addlem  25735  i1fibl  25785  itgitg1  25786  itg2addnclem  38006  itg2addnclem2  38007  itg2addnclem3  38008  itg2addnc  38009  ftc1anclem3  38030  ftc1anclem4  38031  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036