Theorem i1ff 25427

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

Syntax hints:   → wi 4   ∧ w3a 1085   ∈ wcel 2104   ∖ cdif 3946  {csn 4629  ^◡ccnv 5676  dom cdm 5677  ran crn 5678   “ cima 5680  ⟶wf 6540  ‘cfv 6544  Fincfn 8943  ℝcr 11113  0cc0 11114  volcvol 25214  MblFncmbf 25365  ∫₁citg1 25366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-sum 15639  df-itg1 25371

This theorem is referenced by:  i1fima  25429  i1fima2  25430  i1f0rn  25433  itg1val2  25435  itg1cl  25436  itg1ge0  25437  i1faddlem  25444  i1fmullem  25445  i1fadd  25446  i1fmul  25447  itg1addlem4  25450  itg1addlem4OLD  25451  itg1addlem5  25452  i1fmulclem  25454  i1fmulc  25455  itg1mulc  25456  i1fres  25457  i1fpos  25458  i1fposd  25459  i1fsub  25460  itg1sub  25461  itg10a  25462  itg1ge0a  25463  itg1lea  25464  itg1le  25465  itg1climres  25466  mbfi1fseqlem5  25471  mbfi1fseqlem6  25472  mbfi1flimlem  25474  mbfmullem2  25476  itg2itg1  25488  itg20  25489  itg2le  25491  itg2seq  25494  itg2uba  25495  itg2lea  25496  itg2mulclem  25498  itg2splitlem  25500  itg2split  25501  itg2monolem1  25502  itg2i1fseqle  25506  itg2i1fseq  25507  itg2addlem  25510  i1fibl  25559  itgitg1  25560  itg2addnclem  36844  itg2addnclem2  36845  itg2addnclem3  36846  itg2addnc  36847  ftc1anclem3  36868  ftc1anclem4  36869  ftc1anclem5  36870  ftc1anclem6  36871  ftc1anclem7  36872  ftc1anclem8  36873  ftc1anc  36874