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 -1 B = A

Proof

Step Hyp Ref Expression
1 imassrn F -1 B ran F -1
2 dfdm4 dom F = ran F -1
3 fdm F : A B dom F = A
4 ssid A A
5 3 4 eqsstrdi F : A B dom F A
6 2 5 eqsstrrid F : A B ran F -1 A
7 1 6 sstrid F : A B F -1 B A
8 fimass F : A B F A B
9 ffun F : A B Fun F
10 4 3 sseqtrrid F : A B A dom F
11 funimass3 Fun F A dom F F A B A F -1 B
12 9 10 11 syl2anc F : A B F A B A F -1 B
13 8 12 mpbid F : A B A F -1 B
14 7 13 eqssd F : A B F -1 B = A