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\underset{onto}{⟶}B\to G^{-1}\left[B\right]=A$$

Proof

Step	Hyp	Ref	Expression
1		forn	$$⊢G:A\underset{onto}{⟶}B\to \mathrm{ran}G=B$$
2	1	eqcomd	$$⊢G:A\underset{onto}{⟶}B\to B=\mathrm{ran}G$$
3	2	imaeq2d	$$⊢G:A\underset{onto}{⟶}B\to G^{-1}\left[B\right]=G^{-1}\left[\mathrm{ran}G\right]$$
4		cnvimarndm	$$⊢G^{-1}\left[\mathrm{ran}G\right]=\mathrm{dom}G$$
5	3 4	eqtrdi	$$⊢G:A\underset{onto}{⟶}B\to G^{-1}\left[B\right]=\mathrm{dom}G$$
6		fof	$$⊢G:A\underset{onto}{⟶}B\to G:A⟶B$$
7	6	fdmd	$$⊢G:A\underset{onto}{⟶}B\to \mathrm{dom}G=A$$
8	5 7	eqtrd	$$⊢G:A\underset{onto}{⟶}B\to G^{-1}\left[B\right]=A$$