Theorem i1frn 25584

Description: A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.)

Assertion

Ref	Expression
i1frn	⊢ (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)

Proof of Theorem i1frn

Step	Hyp	Ref	Expression
1		isi1f 25581	. . 3 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
2	1	simprbi 496	. 2 ⊢ (𝐹 ∈ dom ∫1 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
3	2	simp2d 1143	1 ⊢ (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109   ∖ cdif 3913  {csn 4591  ^◡ccnv 5639  dom cdm 5640  ran crn 5641   “ cima 5643  ⟶wf 6509  ‘cfv 6513  Fincfn 8920  ℝcr 11073  0cc0 11074  volcvol 25370  MblFncmbf 25521  ∫₁citg1 25522

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 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-fv 6521  df-sum 15659  df-itg1 25527

This theorem is referenced by:  i1fima  25585  itg1cl  25592  itg1ge0  25593  i1fadd  25602  i1fmul  25603  itg1addlem4  25606  itg1addlem5  25607  i1fmulc  25610  itg1mulc  25611  i1fres  25612  itg10a  25617  itg1ge0a  25618  itg1climres  25621  itg2addnclem2  37661  ftc1anclem3  37684  ftc1anclem6  37687  ftc1anclem7  37688  ftc1anc  37690