Theorem i1ff 24821

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

Syntax hints:   → wi 4   ∧ w3a 1085   ∈ wcel 2109   ∖ cdif 3888  {csn 4566  ^◡ccnv 5587  dom cdm 5588  ran crn 5589   “ cima 5591  ⟶wf 6426  ‘cfv 6430  Fincfn 8707  ℝcr 10854  0cc0 10855  volcvol 24608  MblFncmbf 24759  ∫₁citg1 24760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-fv 6438  df-sum 15379  df-itg1 24765

This theorem is referenced by:  i1fima  24823  i1fima2  24824  i1f0rn  24827  itg1val2  24829  itg1cl  24830  itg1ge0  24831  i1faddlem  24838  i1fmullem  24839  i1fadd  24840  i1fmul  24841  itg1addlem4  24844  itg1addlem4OLD  24845  itg1addlem5  24846  i1fmulclem  24848  i1fmulc  24849  itg1mulc  24850  i1fres  24851  i1fpos  24852  i1fposd  24853  i1fsub  24854  itg1sub  24855  itg10a  24856  itg1ge0a  24857  itg1lea  24858  itg1le  24859  itg1climres  24860  mbfi1fseqlem5  24865  mbfi1fseqlem6  24866  mbfi1flimlem  24868  mbfmullem2  24870  itg2itg1  24882  itg20  24883  itg2le  24885  itg2seq  24888  itg2uba  24889  itg2lea  24890  itg2mulclem  24892  itg2splitlem  24894  itg2split  24895  itg2monolem1  24896  itg2i1fseqle  24900  itg2i1fseq  24901  itg2addlem  24904  i1fibl  24953  itgitg1  24954  itg2addnclem  35807  itg2addnclem2  35808  itg2addnclem3  35809  itg2addnc  35810  ftc1anclem3  35831  ftc1anclem4  35832  ftc1anclem5  35833  ftc1anclem6  35834  ftc1anclem7  35835  ftc1anclem8  35836  ftc1anc  35837