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 ( 𝐹 : 𝐴𝐵 → ( 𝐹𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 imassrn ( 𝐹𝐵 ) ⊆ ran 𝐹
2 dfdm4 dom 𝐹 = ran 𝐹
3 fdm ( 𝐹 : 𝐴𝐵 → dom 𝐹 = 𝐴 )
4 ssid 𝐴𝐴
5 3 4 eqsstrdi ( 𝐹 : 𝐴𝐵 → dom 𝐹𝐴 )
6 2 5 eqsstrrid ( 𝐹 : 𝐴𝐵 → ran 𝐹𝐴 )
7 1 6 sstrid ( 𝐹 : 𝐴𝐵 → ( 𝐹𝐵 ) ⊆ 𝐴 )
8 fimass ( 𝐹 : 𝐴𝐵 → ( 𝐹𝐴 ) ⊆ 𝐵 )
9 ffun ( 𝐹 : 𝐴𝐵 → Fun 𝐹 )
10 4 3 sseqtrrid ( 𝐹 : 𝐴𝐵𝐴 ⊆ dom 𝐹 )
11 funimass3 ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹𝐴 ) ⊆ 𝐵𝐴 ⊆ ( 𝐹𝐵 ) ) )
12 9 10 11 syl2anc ( 𝐹 : 𝐴𝐵 → ( ( 𝐹𝐴 ) ⊆ 𝐵𝐴 ⊆ ( 𝐹𝐵 ) ) )
13 8 12 mpbid ( 𝐹 : 𝐴𝐵𝐴 ⊆ ( 𝐹𝐵 ) )
14 7 13 eqssd ( 𝐹 : 𝐴𝐵 → ( 𝐹𝐵 ) = 𝐴 )