Theorem focnvimacdmdm

Description: The preimage of the codomain of a surjection is its domain. (Contributed by AV, 29-Sep-2024)

	Ref	Expression
Assertion	focnvimacdmdm	|- ( G : A -onto-> B -> ( `' G " B ) = A )

Proof

Step	Hyp	Ref	Expression
1		forn	|- ( G : A -onto-> B -> ran G = B )
2	1	eqcomd	|- ( G : A -onto-> B -> B = ran G )
3	2	imaeq2d	|- ( G : A -onto-> B -> ( `' G " B ) = ( `' G " ran G ) )
4		cnvimarndm	|- ( `' G " ran G ) = dom G
5	3 4	eqtrdi	|- ( G : A -onto-> B -> ( `' G " B ) = dom G )
6		fof	|- ( G : A -onto-> B -> G : A --> B )
7	6	fdmd	|- ( G : A -onto-> B -> dom G = A )
8	5 7	eqtrd	|- ( G : A -onto-> B -> ( `' G " B ) = A )