# 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}=\mathrm{SymGrp}\left({A}\right)$
symgbas.2 ${⊢}{B}={\mathrm{Base}}_{{G}}$
Assertion symgfvne ${⊢}\left({F}\in {B}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to \left({F}\left({X}\right)={Z}\to \left({Y}\ne {X}\to {F}\left({Y}\right)\ne {Z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 symgbas.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
2 symgbas.2 ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 1 2 symgbasf1o ${⊢}{F}\in {B}\to {F}:{A}\underset{1-1 onto}{⟶}{A}$
4 f1of1 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{A}\to {F}:{A}\underset{1-1}{⟶}{A}$
5 eqeq2 ${⊢}{Z}={F}\left({X}\right)\to \left({F}\left({Y}\right)={Z}↔{F}\left({Y}\right)={F}\left({X}\right)\right)$
6 5 eqcoms ${⊢}{F}\left({X}\right)={Z}\to \left({F}\left({Y}\right)={Z}↔{F}\left({Y}\right)={F}\left({X}\right)\right)$
7 6 adantl ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\wedge {F}\left({X}\right)={Z}\right)\to \left({F}\left({Y}\right)={Z}↔{F}\left({Y}\right)={F}\left({X}\right)\right)$
8 simp1 ${⊢}\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {F}:{A}\underset{1-1}{⟶}{A}$
9 simp3 ${⊢}\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {Y}\in {A}$
10 simp2 ${⊢}\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {X}\in {A}$
11 f1veqaeq ${⊢}\left({F}:{A}\underset{1-1}{⟶}{A}\wedge \left({Y}\in {A}\wedge {X}\in {A}\right)\right)\to \left({F}\left({Y}\right)={F}\left({X}\right)\to {Y}={X}\right)$
12 8 9 10 11 syl12anc ${⊢}\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to \left({F}\left({Y}\right)={F}\left({X}\right)\to {Y}={X}\right)$
13 12 adantr ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\wedge {F}\left({X}\right)={Z}\right)\to \left({F}\left({Y}\right)={F}\left({X}\right)\to {Y}={X}\right)$
14 7 13 sylbid ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\wedge {F}\left({X}\right)={Z}\right)\to \left({F}\left({Y}\right)={Z}\to {Y}={X}\right)$
15 14 necon3d ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{A}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\wedge {F}\left({X}\right)={Z}\right)\to \left({Y}\ne {X}\to {F}\left({Y}\right)\ne {Z}\right)$
16 15 3exp1 ${⊢}{F}:{A}\underset{1-1}{⟶}{A}\to \left({X}\in {A}\to \left({Y}\in {A}\to \left({F}\left({X}\right)={Z}\to \left({Y}\ne {X}\to {F}\left({Y}\right)\ne {Z}\right)\right)\right)\right)$
17 3 4 16 3syl ${⊢}{F}\in {B}\to \left({X}\in {A}\to \left({Y}\in {A}\to \left({F}\left({X}\right)={Z}\to \left({Y}\ne {X}\to {F}\left({Y}\right)\ne {Z}\right)\right)\right)\right)$
18 17 3imp ${⊢}\left({F}\in {B}\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to \left({F}\left({X}\right)={Z}\to \left({Y}\ne {X}\to {F}\left({Y}\right)\ne {Z}\right)\right)$