Theorem fimacnv

Description: The preimage of the codomain of a function is the function's domain. (Contributed by FL, 25-Jan-2007) (Proof shortened by AV, 20-Sep-2024)

	Ref	Expression
Assertion	fimacnv	$$⊢F:A⟶B\to F^{-1}\left[B\right]=A$$

Proof

Step	Hyp	Ref	Expression
1		frn	$$⊢F:A⟶B\to \mathrm{ran}F\subseteq B$$
2		cnvimassrndm	$$⊢\mathrm{ran}F\subseteq B\to F^{-1}\left[B\right]=\mathrm{dom}F$$
3	1 2	syl	$$⊢F:A⟶B\to F^{-1}\left[B\right]=\mathrm{dom}F$$
4		fdm	$$⊢F:A⟶B\to \mathrm{dom}F=A$$
5	3 4	eqtrd	$$⊢F:A⟶B\to F^{-1}\left[B\right]=A$$