This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem preimane

Description: Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023)

Ref Expression
Hypotheses preimane.f 
|- ( ph -> Fun F )
preimane.x 
|- ( ph -> X =/= Y )
preimane.y 
|- ( ph -> X e. ran F )
preimane.1 
|- ( ph -> Y e. ran F )
Assertion preimane 
|- ( ph -> ( `' F " { X } ) =/= ( `' F " { Y } ) )

Proof

Step Hyp Ref Expression
1 preimane.f 
 |-  ( ph -> Fun F )
2 preimane.x 
 |-  ( ph -> X =/= Y )
3 preimane.y 
 |-  ( ph -> X e. ran F )
4 preimane.1 
 |-  ( ph -> Y e. ran F )
5 sneqrg 
 |-  ( X e. ran F -> ( { X } = { Y } -> X = Y ) )
6 3 5 syl 
 |-  ( ph -> ( { X } = { Y } -> X = Y ) )
7 6 necon3d 
 |-  ( ph -> ( X =/= Y -> { X } =/= { Y } ) )
8 2 7 mpd 
 |-  ( ph -> { X } =/= { Y } )
9 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " { X } ) ) = ( { X } i^i ran F ) )
10 1 9 syl 
 |-  ( ph -> ( F " ( `' F " { X } ) ) = ( { X } i^i ran F ) )
11 3 snssd 
 |-  ( ph -> { X } C_ ran F )
12 dfss2 
 |-  ( { X } C_ ran F <-> ( { X } i^i ran F ) = { X } )
13 11 12 sylib 
 |-  ( ph -> ( { X } i^i ran F ) = { X } )
14 10 13 eqtrd 
 |-  ( ph -> ( F " ( `' F " { X } ) ) = { X } )
15 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " { Y } ) ) = ( { Y } i^i ran F ) )
16 1 15 syl 
 |-  ( ph -> ( F " ( `' F " { Y } ) ) = ( { Y } i^i ran F ) )
17 4 snssd 
 |-  ( ph -> { Y } C_ ran F )
18 dfss2 
 |-  ( { Y } C_ ran F <-> ( { Y } i^i ran F ) = { Y } )
19 17 18 sylib 
 |-  ( ph -> ( { Y } i^i ran F ) = { Y } )
20 16 19 eqtrd 
 |-  ( ph -> ( F " ( `' F " { Y } ) ) = { Y } )
21 8 14 20 3netr4d 
 |-  ( ph -> ( F " ( `' F " { X } ) ) =/= ( F " ( `' F " { Y } ) ) )
22 imaeq2 
 |-  ( ( `' F " { X } ) = ( `' F " { Y } ) -> ( F " ( `' F " { X } ) ) = ( F " ( `' F " { Y } ) ) )
23 22 necon3i 
 |-  ( ( F " ( `' F " { X } ) ) =/= ( F " ( `' F " { Y } ) ) -> ( `' F " { X } ) =/= ( `' F " { Y } ) )
24 21 23 syl 
 |-  ( ph -> ( `' F " { X } ) =/= ( `' F " { Y } ) )