Theorem i1ff 25577

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 25575	. . 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 3911  {csn 4589  ^◡ccnv 5637  dom cdm 5638  ran crn 5639   “ cima 5641  ⟶wf 6507  ‘cfv 6511  Fincfn 8918  ℝcr 11067  0cc0 11068  volcvol 25364  MblFncmbf 25515  ∫₁citg1 25516

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-sum 15653  df-itg1 25521

This theorem is referenced by:  i1fima  25579  i1fima2  25580  i1f0rn  25583  itg1val2  25585  itg1cl  25586  itg1ge0  25587  i1faddlem  25594  i1fmullem  25595  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  itg1addlem5  25601  i1fmulclem  25603  i1fmulc  25604  itg1mulc  25605  i1fres  25606  i1fpos  25607  i1fposd  25608  i1fsub  25609  itg1sub  25610  itg10a  25611  itg1ge0a  25612  itg1lea  25613  itg1le  25614  itg1climres  25615  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  mbfi1flimlem  25623  mbfmullem2  25625  itg2itg1  25637  itg20  25638  itg2le  25640  itg2seq  25643  itg2uba  25644  itg2lea  25645  itg2mulclem  25647  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2i1fseqle  25655  itg2i1fseq  25656  itg2addlem  25659  i1fibl  25709  itgitg1  25710  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem3  37689  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695