Theorem i1ff 25634

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109   ∖ cdif 3928  {csn 4606  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   “ cima 5662  ⟶wf 6532  ‘cfv 6536  Fincfn 8964  ℝcr 11133  0cc0 11134  volcvol 25421  MblFncmbf 25572  ∫₁citg1 25573

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-sum 15708  df-itg1 25578

This theorem is referenced by:  i1fima  25636  i1fima2  25637  i1f0rn  25640  itg1val2  25642  itg1cl  25643  itg1ge0  25644  i1faddlem  25651  i1fmullem  25652  i1fadd  25653  i1fmul  25654  itg1addlem4  25657  itg1addlem5  25658  i1fmulclem  25660  i1fmulc  25661  itg1mulc  25662  i1fres  25663  i1fpos  25664  i1fposd  25665  i1fsub  25666  itg1sub  25667  itg10a  25668  itg1ge0a  25669  itg1lea  25670  itg1le  25671  itg1climres  25672  mbfi1fseqlem5  25677  mbfi1fseqlem6  25678  mbfi1flimlem  25680  mbfmullem2  25682  itg2itg1  25694  itg20  25695  itg2le  25697  itg2seq  25700  itg2uba  25701  itg2lea  25702  itg2mulclem  25704  itg2splitlem  25706  itg2split  25707  itg2monolem1  25708  itg2i1fseqle  25712  itg2i1fseq  25713  itg2addlem  25716  i1fibl  25766  itgitg1  25767  itg2addnclem  37700  itg2addnclem2  37701  itg2addnclem3  37702  itg2addnc  37703  ftc1anclem3  37724  ftc1anclem4  37725  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730