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 )