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		df-ss	|- ( { 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		df-ss	|- ( { 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 } ) )