2f1fvneq

Description: If two one-to-one functions are applied on different arguments, also the values are different. (Contributed by Alexander van der Vekens, 25-Jan-2018) (Proof shortened by AV, 30-Oct-2025)

		Ref	Expression
	Assertion	2f1fvneq	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C) \land A \neq B) \to ((E (F (A)) = X \land E (F (B)) = Y) \to X \neq Y)$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C) \land A \neq B) \to E : D \underset{1-1}{⟶} R$
2		f1f	$⊢ F : C \underset{1-1}{⟶} D \to F : C ⟶ D$
3	2	adantl	$⊢ (E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \to F : C ⟶ D$
4	3	adantr	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to F : C ⟶ D$
5		simpl	$⊢ (A \in C \land B \in C) \to A \in C$
6	5	adantl	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to A \in C$
7	4 6	ffvelcdmd	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to F (A) \in D$
8	7	3adant3	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C) \land A \neq B) \to F (A) \in D$
9		simpr	$⊢ (A \in C \land B \in C) \to B \in C$
10	9	adantl	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to B \in C$
11	4 10	ffvelcdmd	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to F (B) \in D$
12	11	3adant3	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C) \land A \neq B) \to F (B) \in D$
13		simpr	$⊢ (E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \to F : C \underset{1-1}{⟶} D$
14		df-3an	$⊢ (A \in C \land B \in C \land A \neq B) \leftrightarrow ((A \in C \land B \in C) \land A \neq B)$
15	14	biimpri	$⊢ ((A \in C \land B \in C) \land A \neq B) \to (A \in C \land B \in C \land A \neq B)$
16		dff14i	$⊢ (F : C \underset{1-1}{⟶} D \land (A \in C \land B \in C \land A \neq B)) \to F (A) \neq F (B)$
17	13 15 16	syl3an132	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C) \land A \neq B) \to F (A) \neq F (B)$
18		dff14i	$⊢ (E : D \underset{1-1}{⟶} R \land (F (A) \in D \land F (B) \in D \land F (A) \neq F (B))) \to E (F (A)) \neq E (F (B))$
19	1 8 12 17 18	syl13anc	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C) \land A \neq B) \to E (F (A)) \neq E (F (B))$
20		simpl	$⊢ (E (F (A)) = X \land E (F (B)) = Y) \to E (F (A)) = X$
21		simpr	$⊢ (E (F (A)) = X \land E (F (B)) = Y) \to E (F (B)) = Y$
22	20 21	neeq12d	$⊢ (E (F (A)) = X \land E (F (B)) = Y) \to (E (F (A)) \neq E (F (B)) \leftrightarrow X \neq Y)$
23	19 22	syl5ibcom	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C) \land A \neq B) \to ((E (F (A)) = X \land E (F (B)) = Y) \to X \neq Y)$

Metamath Proof Explorer

Theorem 2f1fvneq

Proof