Metamath Proof Explorer


Theorem fimacnvOLD

Description: Obsolete version of fimacnv as of 20-Sep-2024. (Contributed by FL, 25-Jan-2007) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion fimacnvOLD
|- ( F : A --> B -> ( `' F " B ) = A )

Proof

Step Hyp Ref Expression
1 imassrn
 |-  ( `' F " B ) C_ ran `' F
2 dfdm4
 |-  dom F = ran `' F
3 fdm
 |-  ( F : A --> B -> dom F = A )
4 ssid
 |-  A C_ A
5 3 4 eqsstrdi
 |-  ( F : A --> B -> dom F C_ A )
6 2 5 eqsstrrid
 |-  ( F : A --> B -> ran `' F C_ A )
7 1 6 sstrid
 |-  ( F : A --> B -> ( `' F " B ) C_ A )
8 fimass
 |-  ( F : A --> B -> ( F " A ) C_ B )
9 ffun
 |-  ( F : A --> B -> Fun F )
10 4 3 sseqtrrid
 |-  ( F : A --> B -> A C_ dom F )
11 funimass3
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )
12 9 10 11 syl2anc
 |-  ( F : A --> B -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )
13 8 12 mpbid
 |-  ( F : A --> B -> A C_ ( `' F " B ) )
14 7 13 eqssd
 |-  ( F : A --> B -> ( `' F " B ) = A )