This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rescnvimafod

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)

Ref Expression
Hypotheses rescnvimafod.f ⊢ φ → F Fn A
rescnvimafod.e ⊢ φ → E = ran ⁡ F ∩ B
rescnvimafod.d ⊢ φ → D = F -1 B
Assertion rescnvimafod ⊢ φ → F ↾ D : D ⟶ onto E

Proof

Step Hyp Ref Expression
1 rescnvimafod.f ⊢ φ → F Fn A
2 rescnvimafod.e ⊢ φ → E = ran ⁡ F ∩ B
3 rescnvimafod.d ⊢ φ → D = F -1 B
4 cnvimass ⊢ F -1 B ⊆ dom ⁡ F
5 4 a1i ⊢ φ → F -1 B ⊆ dom ⁡ F
6 1 fndmd ⊢ φ → dom ⁡ F = A
7 6 eqcomd ⊢ φ → A = dom ⁡ F
8 5 3 7 3sstr4d ⊢ φ → D ⊆ A
9 1 8 fnssresd ⊢ φ → F ↾ D Fn D
10 df-ima ⊢ F D = ran ⁡ F ↾ D
11 3 imaeq2d ⊢ φ → F D = F F -1 B
12 fnfun ⊢ F Fn A → Fun ⁡ F
13 funimacnv ⊢ Fun ⁡ F → F F -1 B = B ∩ ran ⁡ F
14 1 12 13 3syl ⊢ φ → F F -1 B = B ∩ ran ⁡ F
15 incom ⊢ B ∩ ran ⁡ F = ran ⁡ F ∩ B
16 15 a1i ⊢ φ → B ∩ ran ⁡ F = ran ⁡ F ∩ B
17 11 14 16 3eqtrd ⊢ φ → F D = ran ⁡ F ∩ B
18 10 17 eqtr3id ⊢ φ → ran ⁡ F ↾ D = ran ⁡ F ∩ B
19 18 2 eqtr4d ⊢ φ → ran ⁡ F ↾ D = E
20 df-fo ⊢ F ↾ D : D ⟶ onto E ↔ F ↾ D Fn D ∧ ran ⁡ F ↾ D = E
21 9 19 20 sylanbrc ⊢ φ → F ↾ D : D ⟶ onto E