# Metamath Proof Explorer

## 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}↔{A}\subseteq {{F}}^{-1}\left[{B}\right]\right)$
12 9 10 11 syl2anc ${⊢}{F}:{A}⟶{B}\to \left({F}\left[{A}\right]\subseteq {B}↔{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}$