Theorem i1ff 24376

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

Syntax hints:   → wi 4   ∧ w3a 1084   ∈ wcel 2111   ∖ cdif 3855  {csn 4522  ^◡ccnv 5523  dom cdm 5524  ran crn 5525   “ cima 5527  ⟶wf 6331  ‘cfv 6335  Fincfn 8527  ℝcr 10574  0cc0 10575  volcvol 24163  MblFncmbf 24314  ∫₁citg1 24315

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-fv 6343  df-sum 15091  df-itg1 24320

This theorem is referenced by:  i1fima  24378  i1fima2  24379  i1f0rn  24382  itg1val2  24384  itg1cl  24385  itg1ge0  24386  i1faddlem  24393  i1fmullem  24394  i1fadd  24395  i1fmul  24396  itg1addlem4  24399  itg1addlem5  24400  i1fmulclem  24402  i1fmulc  24403  itg1mulc  24404  i1fres  24405  i1fpos  24406  i1fposd  24407  i1fsub  24408  itg1sub  24409  itg10a  24410  itg1ge0a  24411  itg1lea  24412  itg1le  24413  itg1climres  24414  mbfi1fseqlem5  24419  mbfi1fseqlem6  24420  mbfi1flimlem  24422  mbfmullem2  24424  itg2itg1  24436  itg20  24437  itg2le  24439  itg2seq  24442  itg2uba  24443  itg2lea  24444  itg2mulclem  24446  itg2splitlem  24448  itg2split  24449  itg2monolem1  24450  itg2i1fseqle  24454  itg2i1fseq  24455  itg2addlem  24458  i1fibl  24507  itgitg1  24508  itg2addnclem  35388  itg2addnclem2  35389  itg2addnclem3  35390  itg2addnc  35391  ftc1anclem3  35412  ftc1anclem4  35413  ftc1anclem5  35414  ftc1anclem6  35415  ftc1anclem7  35416  ftc1anclem8  35417  ftc1anc  35418