Theorem i1ff 23663

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

Syntax hints:   → wi 4   ∧ w3a 1072   ∈ wcel 2140   ∖ cdif 3713  {csn 4322  ^◡ccnv 5266  dom cdm 5267  ran crn 5268   “ cima 5270  ⟶wf 6046  ‘cfv 6050  Fincfn 8124  ℝcr 10148  0cc0 10149  volcvol 23453  MblFncmbf 23603  ∫₁citg1 23604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pr 5056

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-fv 6058  df-sum 14637  df-itg1 23609

This theorem is referenced by:  i1fima  23665  i1fima2  23666  i1f0rn  23669  itg1val2  23671  itg1cl  23672  itg1ge0  23673  i1faddlem  23680  i1fmullem  23681  i1fadd  23682  i1fmul  23683  itg1addlem4  23686  itg1addlem5  23687  i1fmulclem  23689  i1fmulc  23690  itg1mulc  23691  i1fres  23692  i1fpos  23693  i1fposd  23694  i1fsub  23695  itg1sub  23696  itg10a  23697  itg1ge0a  23698  itg1lea  23699  itg1le  23700  itg1climres  23701  mbfi1fseqlem5  23706  mbfi1fseqlem6  23707  mbfi1flimlem  23709  mbfmullem2  23711  itg2itg1  23723  itg20  23724  itg2le  23726  itg2seq  23729  itg2uba  23730  itg2lea  23731  itg2mulclem  23733  itg2splitlem  23735  itg2split  23736  itg2monolem1  23737  itg2i1fseqle  23741  itg2i1fseq  23742  itg2addlem  23745  i1fibl  23794  itgitg1  23795  itg2addnclem  33793  itg2addnclem2  33794  itg2addnclem3  33795  itg2addnc  33796  ftc1anclem3  33819  ftc1anclem4  33820  ftc1anclem5  33821  ftc1anclem6  33822  ftc1anclem7  33823  ftc1anclem8  33824  ftc1anc  33825