Theorem i1ff 24889

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2104   ∖ cdif 3889  {csn 4565  ^◡ccnv 5599  dom cdm 5600  ran crn 5601   “ cima 5603  ⟶wf 6454  ‘cfv 6458  Fincfn 8764  ℝcr 10920  0cc0 10921  volcvol 24676  MblFncmbf 24827  ∫₁citg1 24828

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 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3306  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-fv 6466  df-sum 15447  df-itg1 24833

This theorem is referenced by:  i1fima  24891  i1fima2  24892  i1f0rn  24895  itg1val2  24897  itg1cl  24898  itg1ge0  24899  i1faddlem  24906  i1fmullem  24907  i1fadd  24908  i1fmul  24909  itg1addlem4  24912  itg1addlem4OLD  24913  itg1addlem5  24914  i1fmulclem  24916  i1fmulc  24917  itg1mulc  24918  i1fres  24919  i1fpos  24920  i1fposd  24921  i1fsub  24922  itg1sub  24923  itg10a  24924  itg1ge0a  24925  itg1lea  24926  itg1le  24927  itg1climres  24928  mbfi1fseqlem5  24933  mbfi1fseqlem6  24934  mbfi1flimlem  24936  mbfmullem2  24938  itg2itg1  24950  itg20  24951  itg2le  24953  itg2seq  24956  itg2uba  24957  itg2lea  24958  itg2mulclem  24960  itg2splitlem  24962  itg2split  24963  itg2monolem1  24964  itg2i1fseqle  24968  itg2i1fseq  24969  itg2addlem  24972  i1fibl  25021  itgitg1  25022  itg2addnclem  35876  itg2addnclem2  35877  itg2addnclem3  35878  itg2addnc  35879  ftc1anclem3  35900  ftc1anclem4  35901  ftc1anclem5  35902  ftc1anclem6  35903  ftc1anclem7  35904  ftc1anclem8  35905  ftc1anc  35906