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 \in B \land X \in A \land Y \in A) \to (F (X) = Z \to (Y \neq X \to F (Y) \neq Z))$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$⊢ G = SymGrp (A)$
2		symgbas.2	$⊢ B = {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 (X) \to (F (Y) = Z \leftrightarrow F (Y) = F (X))$
6	5	eqcoms	$⊢ F (X) = Z \to (F (Y) = Z \leftrightarrow F (Y) = F (X))$
7	6	adantl	$⊢ ((F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \land F (X) = Z) \to (F (Y) = Z \leftrightarrow F (Y) = F (X))$
8		simp1	$⊢ (F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \to F : A \underset{1-1}{⟶} A$
9		simp3	$⊢ (F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \to Y \in A$
10		simp2	$⊢ (F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \to X \in A$
11		f1veqaeq	$⊢ (F : A \underset{1-1}{⟶} A \land (Y \in A \land X \in A)) \to (F (Y) = F (X) \to Y = X)$
12	8 9 10 11	syl12anc	$⊢ (F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \to (F (Y) = F (X) \to Y = X)$
13	12	adantr	$⊢ ((F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \land F (X) = Z) \to (F (Y) = F (X) \to Y = X)$
14	7 13	sylbid	$⊢ ((F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \land F (X) = Z) \to (F (Y) = Z \to Y = X)$
15	14	necon3d	$⊢ ((F : A \underset{1-1}{⟶} A \land X \in A \land Y \in A) \land F (X) = Z) \to (Y \neq X \to F (Y) \neq Z)$
16	15	3exp1	$⊢ F : A \underset{1-1}{⟶} A \to (X \in A \to (Y \in A \to (F (X) = Z \to (Y \neq X \to F (Y) \neq Z))))$
17	3 4 16	3syl	$⊢ F \in B \to (X \in A \to (Y \in A \to (F (X) = Z \to (Y \neq X \to F (Y) \neq Z))))$
18	17	3imp	$⊢ (F \in B \land X \in A \land Y \in A) \to (F (X) = Z \to (Y \neq X \to F (Y) \neq Z))$