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

Metamath Proof Explorer

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 ) ) )