Theorem i1ff 25866

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2146   ∖ cdif 3903  {csn 4591  ^◡ccnv 5662  dom cdm 5663  ran crn 5664   “ cima 5666  ⟶wf 6536  ‘cfv 6540  Fincfn 8945  ℝcr 11110  0cc0 11111  volcvol 25653  MblFncmbf 25804  ∫₁citg1 25805

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-sum 15758  df-itg1 25810

This theorem is used by:  i1fima  25868  i1fima2  25869  i1f0rn  25872  itg1val2  25874  itg1cl  25875  itg1ge0  25876  i1faddlem  25883  i1fmullem  25884  i1fadd  25885  i1fmul  25886  itg1addlem4  25889  itg1addlem5  25890  i1fmulclem  25892  i1fmulc  25893  itg1mulc  25894  i1fres  25895  i1fpos  25896  i1fposd  25897  i1fsub  25898  itg1sub  25899  itg10a  25900  itg1ge0a  25901  itg1lea  25902  itg1le  25903  itg1climres  25904  mbfi1fseqlem5  25909  mbfi1fseqlem6  25910  mbfi1flimlem  25912  mbfmullem2  25914  itg2itg1  25926  itg20  25927  itg2le  25929  itg2seq  25932  itg2uba  25933  itg2lea  25934  itg2mulclem  25936  itg2splitlem  25938  itg2split  25939  itg2monolem1  25940  itg2i1fseqle  25944  itg2i1fseq  25945  itg2addlem  25948  i1fibl  25998  itgitg1  25999  itg2addnclem  38355  itg2addnclem2  38356  itg2addnclem3  38357  itg2addnc  38358  ftc1anclem3  38379  ftc1anclem4  38380  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385