Theorem i1ff 25665

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

Syntax hints:   → wi 4   ∧ w3a 1093   ∈ wcel 2121   ∖ cdif 3882  {csn 4558  ^◡ccnv 5620  dom cdm 5621  ran crn 5622   “ cima 5624  ⟶wf 6485  ‘cfv 6489  Fincfn 8887  ℝcr 11032  0cc0 11033  volcvol 25452  MblFncmbf 25603  ∫₁citg1 25604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497  df-sum 15644  df-itg1 25609

This theorem is referenced by:  i1fima  25667  i1fima2  25668  i1f0rn  25671  itg1val2  25673  itg1cl  25674  itg1ge0  25675  i1faddlem  25682  i1fmullem  25683  i1fadd  25684  i1fmul  25685  itg1addlem4  25688  itg1addlem5  25689  i1fmulclem  25691  i1fmulc  25692  itg1mulc  25693  i1fres  25694  i1fpos  25695  i1fposd  25696  i1fsub  25697  itg1sub  25698  itg10a  25699  itg1ge0a  25700  itg1lea  25701  itg1le  25702  itg1climres  25703  mbfi1fseqlem5  25708  mbfi1fseqlem6  25709  mbfi1flimlem  25711  mbfmullem2  25713  itg2itg1  25725  itg20  25726  itg2le  25728  itg2seq  25731  itg2uba  25732  itg2lea  25733  itg2mulclem  25735  itg2splitlem  25737  itg2split  25738  itg2monolem1  25739  itg2i1fseqle  25743  itg2i1fseq  25744  itg2addlem  25747  i1fibl  25797  itgitg1  25798  itg2addnclem  38053  itg2addnclem2  38054  itg2addnclem3  38055  itg2addnc  38056  ftc1anclem3  38077  ftc1anclem4  38078  ftc1anclem5  38079  ftc1anclem6  38080  ftc1anclem7  38081  ftc1anclem8  38082  ftc1anc  38083