Theorem fimacnv

Description: The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007)

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

Proof

Step	Hyp	Ref	Expression
1		imassrn	$$⊢F^{-1}\left[B\right]\subseteq \mathrm{ran}{F}^{-1}$$
2		dfdm4	$$⊢\mathrm{dom}F=\mathrm{ran}{F}^{-1}$$
3		fdm	$$⊢F:A⟶B\to \mathrm{dom}F=A$$
4		ssid	$$⊢A\subseteq A$$
5	3 4	eqsstrdi	$$⊢F:A⟶B\to \mathrm{dom}F\subseteq A$$
6	2 5	eqsstrrid	$$⊢F:A⟶B\to \mathrm{ran}{F}^{-1}\subseteq A$$
7	1 6	sstrid	$$⊢F:A⟶B\to F^{-1}\left[B\right]\subseteq A$$
8		fimass	$$⊢F:A⟶B\to F\left[A\right]\subseteq B$$
9		ffun	$$⊢F:A⟶B\to \mathrm{Fun}F$$
10	4 3	sseqtrrid	$$⊢F:A⟶B\to A\subseteq \mathrm{dom}F$$
11		funimass3	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(F\left[A\right]\subseteq B\leftrightarrow A\subseteq F^{-1}\left[B\right]\right)$$
12	9 10 11	syl2anc	$$⊢F:A⟶B\to \left(F\left[A\right]\subseteq B\leftrightarrow A\subseteq F^{-1}\left[B\right]\right)$$
13	8 12	mpbid	$$⊢F:A⟶B\to A\subseteq F^{-1}\left[B\right]$$
14	7 13	eqssd	$$⊢F:A⟶B\to F^{-1}\left[B\right]=A$$