MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rescnvimafod Structured version   Visualization version   GIF version

Theorem rescnvimafod 7092
Description: The restriction of a function to a preimage of a class is a function onto the intersection of this class and the range of the function. (Contributed by AV, 13-Sep-2024.) (Revised by AV, 29-Sep-2024.)
Hypotheses
Ref Expression
rescnvimafod.f (𝜑𝐹 Fn 𝐴)
rescnvimafod.e (𝜑𝐸 = (ran 𝐹𝐵))
rescnvimafod.d (𝜑𝐷 = (𝐹𝐵))
Assertion
Ref Expression
rescnvimafod (𝜑 → (𝐹𝐷):𝐷onto𝐸)

Proof of Theorem rescnvimafod
StepHypRef Expression
1 rescnvimafod.f . . 3 (𝜑𝐹 Fn 𝐴)
2 cnvimass 6101 . . . . 5 (𝐹𝐵) ⊆ dom 𝐹
32a1i 11 . . . 4 (𝜑 → (𝐹𝐵) ⊆ dom 𝐹)
4 rescnvimafod.d . . . 4 (𝜑𝐷 = (𝐹𝐵))
51fndmd 6673 . . . . 5 (𝜑 → dom 𝐹 = 𝐴)
65eqcomd 2740 . . . 4 (𝜑𝐴 = dom 𝐹)
73, 4, 63sstr4d 4042 . . 3 (𝜑𝐷𝐴)
81, 7fnssresd 6692 . 2 (𝜑 → (𝐹𝐷) Fn 𝐷)
9 df-ima 5701 . . . 4 (𝐹𝐷) = ran (𝐹𝐷)
104imaeq2d 6079 . . . . 5 (𝜑 → (𝐹𝐷) = (𝐹 “ (𝐹𝐵)))
11 fnfun 6668 . . . . . 6 (𝐹 Fn 𝐴 → Fun 𝐹)
12 funimacnv 6648 . . . . . 6 (Fun 𝐹 → (𝐹 “ (𝐹𝐵)) = (𝐵 ∩ ran 𝐹))
131, 11, 123syl 18 . . . . 5 (𝜑 → (𝐹 “ (𝐹𝐵)) = (𝐵 ∩ ran 𝐹))
14 incom 4216 . . . . . 6 (𝐵 ∩ ran 𝐹) = (ran 𝐹𝐵)
1514a1i 11 . . . . 5 (𝜑 → (𝐵 ∩ ran 𝐹) = (ran 𝐹𝐵))
1610, 13, 153eqtrd 2778 . . . 4 (𝜑 → (𝐹𝐷) = (ran 𝐹𝐵))
179, 16eqtr3id 2788 . . 3 (𝜑 → ran (𝐹𝐷) = (ran 𝐹𝐵))
18 rescnvimafod.e . . 3 (𝜑𝐸 = (ran 𝐹𝐵))
1917, 18eqtr4d 2777 . 2 (𝜑 → ran (𝐹𝐷) = 𝐸)
20 df-fo 6568 . 2 ((𝐹𝐷):𝐷onto𝐸 ↔ ((𝐹𝐷) Fn 𝐷 ∧ ran (𝐹𝐷) = 𝐸))
218, 19, 20sylanbrc 583 1 (𝜑 → (𝐹𝐷):𝐷onto𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1536  cin 3961  wss 3962  ccnv 5687  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  Fun wfun 6556   Fn wfn 6557  ontowfo 6560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-fo 6568
This theorem is referenced by:  fresfo  46997  fcoreslem3  47014  3f1oss1  47024
  Copyright terms: Public domain W3C validator