Theorem i1ff 25726

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

Syntax hints:   → wi 4   ∧ w3a 1097   ∈ wcel 2141   ∖ cdif 3899  {csn 4579  ^◡ccnv 5642  dom cdm 5643  ran crn 5644   “ cima 5646  ⟶wf 6512  ‘cfv 6516  Fincfn 8921  ℝcr 11066  0cc0 11067  volcvol 25513  MblFncmbf 25664  ∫₁citg1 25665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-fv 6524  df-sum 15705  df-itg1 25670

This theorem is referenced by:  i1fima  25728  i1fima2  25729  i1f0rn  25732  itg1val2  25734  itg1cl  25735  itg1ge0  25736  i1faddlem  25743  i1fmullem  25744  i1fadd  25745  i1fmul  25746  itg1addlem4  25749  itg1addlem5  25750  i1fmulclem  25752  i1fmulc  25753  itg1mulc  25754  i1fres  25755  i1fpos  25756  i1fposd  25757  i1fsub  25758  itg1sub  25759  itg10a  25760  itg1ge0a  25761  itg1lea  25762  itg1le  25763  itg1climres  25764  mbfi1fseqlem5  25769  mbfi1fseqlem6  25770  mbfi1flimlem  25772  mbfmullem2  25774  itg2itg1  25786  itg20  25787  itg2le  25789  itg2seq  25792  itg2uba  25793  itg2lea  25794  itg2mulclem  25796  itg2splitlem  25798  itg2split  25799  itg2monolem1  25800  itg2i1fseqle  25804  itg2i1fseq  25805  itg2addlem  25808  i1fibl  25858  itgitg1  25859  itg2addnclem  38131  itg2addnclem2  38132  itg2addnclem3  38133  itg2addnc  38134  ftc1anclem3  38155  ftc1anclem4  38156  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161