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 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
rescnvimafod.e ⊢ ( 𝜑 → 𝐸 = ( ran 𝐹 ∩ 𝐵 ) )
rescnvimafod.d ⊢ ( 𝜑 → 𝐷 = ( ◡ 𝐹 “ 𝐵 ) )
Assertion rescnvimafod ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ 𝐸 )

Proof

Step Hyp Ref Expression
1 rescnvimafod.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 rescnvimafod.e ⊢ ( 𝜑 → 𝐸 = ( ran 𝐹 ∩ 𝐵 ) )
3 rescnvimafod.d ⊢ ( 𝜑 → 𝐷 = ( ◡ 𝐹 “ 𝐵 ) )
4 cnvimass ⊢ ( ◡ 𝐹 “ 𝐵 ) ⊆ dom 𝐹
5 4 a1i ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐵 ) ⊆ dom 𝐹 )
6 1 fndmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
7 6 eqcomd ⊢ ( 𝜑 → 𝐴 = dom 𝐹 )
8 5 3 7 3sstr4d ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
9 1 8 fnssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) Fn 𝐷 )
10 df-ima ⊢ ( 𝐹 “ 𝐷 ) = ran ( 𝐹 ↾ 𝐷 )
11 3 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ 𝐷 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝐵 ) ) )
12 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
13 funimacnv ⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐵 ) ) = ( 𝐵 ∩ ran 𝐹 ) )
14 1 12 13 3syl ⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐵 ) ) = ( 𝐵 ∩ ran 𝐹 ) )
15 incom ⊢ ( 𝐵 ∩ ran 𝐹 ) = ( ran 𝐹 ∩ 𝐵 )
16 15 a1i ⊢ ( 𝜑 → ( 𝐵 ∩ ran 𝐹 ) = ( ran 𝐹 ∩ 𝐵 ) )
17 11 14 16 3eqtrd ⊢ ( 𝜑 → ( 𝐹 “ 𝐷 ) = ( ran 𝐹 ∩ 𝐵 ) )
18 10 17 eqtr3id ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝐷 ) = ( ran 𝐹 ∩ 𝐵 ) )
19 18 2 eqtr4d ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝐷 ) = 𝐸 )
20 df-fo ⊢ ( ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ 𝐸 ↔ ( ( 𝐹 ↾ 𝐷 ) Fn 𝐷 ∧ ran ( 𝐹 ↾ 𝐷 ) = 𝐸 ) )
21 9 19 20 sylanbrc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ 𝐸 )