Theorem i1ff 26052

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 26050	. . 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 2147   ∖ cdif 4048  {csn 4588  ^◡ccnv 5657  dom cdm 5658  ran crn 5659   “ cima 5661  ⟶wf 6562  ‘cfv 6566  Fincfn 9011  ℝcr 11238  0cc0 11239  volcvol 25839  MblFncmbf 25990  ∫₁citg1 25991

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-sum 15898  df-itg1 25996

This theorem is used by:  i1fima  26054  i1fima2  26055  i1f0rn  26058  itg1val2  26060  itg1cl  26061  itg1ge0  26062  i1faddlem  26069  i1fmullem  26070  i1fadd  26071  i1fmul  26072  itg1addlem4  26075  itg1addlem5  26076  i1fmulclem  26078  i1fmulc  26079  itg1mulc  26080  i1fres  26081  i1fpos  26082  i1fposd  26083  i1fsub  26084  itg1sub  26085  itg10a  26086  itg1ge0a  26087  itg1lea  26088  itg1le  26089  itg1climres  26090  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  mbfi1flimlem  26098  mbfmullem2  26100  itg2itg1  26112  itg20  26113  itg2le  26115  itg2seq  26118  itg2uba  26119  itg2lea  26120  itg2mulclem  26122  itg2splitlem  26124  itg2split  26125  itg2monolem1  26126  itg2i1fseqle  26130  itg2i1fseq  26131  itg2addlem  26134  i1fibl  26183  itgitg1  26184  itg2addnclem  38857  itg2addnclem2  38858  itg2addnclem3  38859  itg2addnc  38860  ftc1anclem3  38881  ftc1anclem4  38882  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anclem8  38886  ftc1anc  38887