Theorem symgfvne

Description: The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019)

	Ref	Expression
Hypotheses	symgbas.1	|- G = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	symgfvne	|- ( ( F e. B /\ X e. A /\ Y e. A ) -> ( ( F ` X ) = Z -> ( Y =/= X -> ( F ` Y ) =/= Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	|- G = ( SymGrp ` A )
2		symgbas.2	|- B = ( Base ` G )
3	1 2	symgbasf1o	|- ( F e. B -> F : A -1-1-onto-> A )
4		f1of1	|- ( F : A -1-1-onto-> A -> F : A -1-1-> A )
5		eqeq2	|- ( Z = ( F ` X ) -> ( ( F ` Y ) = Z <-> ( F ` Y ) = ( F ` X ) ) )
6	5	eqcoms	|- ( ( F ` X ) = Z -> ( ( F ` Y ) = Z <-> ( F ` Y ) = ( F ` X ) ) )
7	6	adantl	|- ( ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) /\ ( F ` X ) = Z ) -> ( ( F ` Y ) = Z <-> ( F ` Y ) = ( F ` X ) ) )
8		simp1	|- ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) -> F : A -1-1-> A )
9		simp3	|- ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) -> Y e. A )
10		simp2	|- ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) -> X e. A )
11		f1veqaeq	|- ( ( F : A -1-1-> A /\ ( Y e. A /\ X e. A ) ) -> ( ( F ` Y ) = ( F ` X ) -> Y = X ) )
12	8 9 10 11	syl12anc	|- ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) -> ( ( F ` Y ) = ( F ` X ) -> Y = X ) )
13	12	adantr	|- ( ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) /\ ( F ` X ) = Z ) -> ( ( F ` Y ) = ( F ` X ) -> Y = X ) )
14	7 13	sylbid	|- ( ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) /\ ( F ` X ) = Z ) -> ( ( F ` Y ) = Z -> Y = X ) )
15	14	necon3d	|- ( ( ( F : A -1-1-> A /\ X e. A /\ Y e. A ) /\ ( F ` X ) = Z ) -> ( Y =/= X -> ( F ` Y ) =/= Z ) )
16	15	3exp1	|- ( F : A -1-1-> A -> ( X e. A -> ( Y e. A -> ( ( F ` X ) = Z -> ( Y =/= X -> ( F ` Y ) =/= Z ) ) ) ) )
17	3 4 16	3syl	|- ( F e. B -> ( X e. A -> ( Y e. A -> ( ( F ` X ) = Z -> ( Y =/= X -> ( F ` Y ) =/= Z ) ) ) ) )
18	17	3imp	|- ( ( F e. B /\ X e. A /\ Y e. A ) -> ( ( F ` X ) = Z -> ( Y =/= X -> ( F ` Y ) =/= Z ) ) )