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→ 𝐸 )