Theorem i1ff 23843

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

Syntax hints:   → wi 4   ∧ w3a 1113   ∈ wcel 2166   ∖ cdif 3796  {csn 4398  ^◡ccnv 5342  dom cdm 5343  ran crn 5344   “ cima 5346  ⟶wf 6120  ‘cfv 6124  Fincfn 8223  ℝcr 10252  0cc0 10253  volcvol 23630  MblFncmbf 23781  ∫₁citg1 23782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pr 5128

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-fv 6132  df-sum 14795  df-itg1 23787

This theorem is referenced by:  i1fima  23845  i1fima2  23846  i1f0rn  23849  itg1val2  23851  itg1cl  23852  itg1ge0  23853  i1faddlem  23860  i1fmullem  23861  i1fadd  23862  i1fmul  23863  itg1addlem4  23866  itg1addlem5  23867  i1fmulclem  23869  i1fmulc  23870  itg1mulc  23871  i1fres  23872  i1fpos  23873  i1fposd  23874  i1fsub  23875  itg1sub  23876  itg10a  23877  itg1ge0a  23878  itg1lea  23879  itg1le  23880  itg1climres  23881  mbfi1fseqlem5  23886  mbfi1fseqlem6  23887  mbfi1flimlem  23889  mbfmullem2  23891  itg2itg1  23903  itg20  23904  itg2le  23906  itg2seq  23909  itg2uba  23910  itg2lea  23911  itg2mulclem  23913  itg2splitlem  23915  itg2split  23916  itg2monolem1  23917  itg2i1fseqle  23921  itg2i1fseq  23922  itg2addlem  23925  i1fibl  23974  itgitg1  23975  itg2addnclem  34005  itg2addnclem2  34006  itg2addnclem3  34007  itg2addnc  34008  ftc1anclem3  34031  ftc1anclem4  34032  ftc1anclem5  34033  ftc1anclem6  34034  ftc1anclem7  34035  ftc1anclem8  34036  ftc1anc  34037