Theorem focnvimacdmdm

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

	Ref	Expression
Assertion	focnvimacdmdm	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		forn	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → ran 𝐺 = 𝐵 )
2	1	eqcomd	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → 𝐵 = ran 𝐺 )
3	2	imaeq2d	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = ( ◡ 𝐺 “ ran 𝐺 ) )
4		cnvimarndm	⊢ ( ◡ 𝐺 “ ran 𝐺 ) = dom 𝐺
5	3 4	eqtrdi	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = dom 𝐺 )
6		fof	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → 𝐺 : 𝐴 ⟶ 𝐵 )
7	6	fdmd	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → dom 𝐺 = 𝐴 )
8	5 7	eqtrd	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = 𝐴 )