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)

		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		f1veqaeq	$⊢ (F : C \underset{1-1}{⟶} D \land (A \in C \land B \in C)) \to (F (A) = F (B) \to A = B)$
2	1	adantll	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to (F (A) = F (B) \to A = B)$
3	2	necon3ad	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to (A \neq B \to \neg F (A) = F (B))$
4	3	3impia	$⊢ ((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 \neg F (A) = F (B)$
5		simpll	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to E : D \underset{1-1}{⟶} R$
6		f1f	$⊢ F : C \underset{1-1}{⟶} D \to F : C ⟶ D$
7		ffvelrn	$⊢ (F : C ⟶ D \land A \in C) \to F (A) \in D$
8		ffvelrn	$⊢ (F : C ⟶ D \land B \in C) \to F (B) \in D$
9	7 8	anim12dan	$⊢ (F : C ⟶ D \land (A \in C \land B \in C)) \to (F (A) \in D \land F (B) \in D)$
10	9	ex	$⊢ F : C ⟶ D \to ((A \in C \land B \in C) \to (F (A) \in D \land F (B) \in D))$
11	6 10	syl	$⊢ F : C \underset{1-1}{⟶} D \to ((A \in C \land B \in C) \to (F (A) \in D \land F (B) \in D))$
12	11	adantl	$⊢ (E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \to ((A \in C \land B \in C) \to (F (A) \in D \land F (B) \in D))$
13	12	imp	$⊢ ((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 \land F (B) \in D)$
14		f1veqaeq	$⊢ (E : D \underset{1-1}{⟶} R \land (F (A) \in D \land F (B) \in D)) \to (E (F (A)) = E (F (B)) \to F (A) = F (B))$
15	5 13 14	syl2anc	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to (E (F (A)) = E (F (B)) \to F (A) = F (B))$
16	15	con3dimp	$⊢ (((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \land \neg F (A) = F (B)) \to \neg E (F (A)) = E (F (B))$
17		eqeq12	$⊢ (E (F (A)) = X \land E (F (B)) = Y) \to (E (F (A)) = E (F (B)) \leftrightarrow X = Y)$
18	17	notbid	$⊢ (E (F (A)) = X \land E (F (B)) = Y) \to (\neg E (F (A)) = E (F (B)) \leftrightarrow \neg X = Y)$
19		neqne	$⊢ \neg X = Y \to X \neq Y$
20	18 19	syl6bi	$⊢ (E (F (A)) = X \land E (F (B)) = Y) \to (\neg E (F (A)) = E (F (B)) \to X \neq Y)$
21	16 20	syl5com	$⊢ (((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \land \neg F (A) = F (B)) \to ((E (F (A)) = X \land E (F (B)) = Y) \to X \neq Y)$
22	21	ex	$⊢ ((E : D \underset{1-1}{⟶} R \land F : C \underset{1-1}{⟶} D) \land (A \in C \land B \in C)) \to (\neg F (A) = F (B) \to ((E (F (A)) = X \land E (F (B)) = Y) \to X \neq Y))$
23	22	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 (\neg F (A) = F (B) \to ((E (F (A)) = X \land E (F (B)) = Y) \to X \neq Y))$
24	4 23	mpd	$⊢ ((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