fvf1pr

Description: Values of a one-to-one function between two sets with two elements. Actually, such a function is a bijection. (Contributed by AV, 22-Jul-2025)

		Ref	Expression
	Assertion	fvf1pr	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X))$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \to F : \{A, B\} ⟶ \{X, Y\}$
2		prid1g	$⊢ A \in V \to A \in \{A, B\}$
3	2	3ad2ant1	$⊢ (A \in V \land B \in W \land A \neq B) \to A \in \{A, B\}$
4		ffvelcdm	$⊢ (F : \{A, B\} ⟶ \{X, Y\} \land A \in \{A, B\}) \to F (A) \in \{X, Y\}$
5	1 3 4	syl2anr	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to F (A) \in \{X, Y\}$
6		prid2g	$⊢ B \in W \to B \in \{A, B\}$
7	6	3ad2ant2	$⊢ (A \in V \land B \in W \land A \neq B) \to B \in \{A, B\}$
8		ffvelcdm	$⊢ (F : \{A, B\} ⟶ \{X, Y\} \land B \in \{A, B\}) \to F (B) \in \{X, Y\}$
9	1 7 8	syl2anr	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to F (B) \in \{X, Y\}$
10		elpri	$⊢ F (A) \in \{X, Y\} \to (F (A) = X \lor F (A) = Y)$
11		elpri	$⊢ F (B) \in \{X, Y\} \to (F (B) = X \lor F (B) = Y)$
12		eqtr3	$⊢ (F (A) = X \land F (B) = X) \to F (A) = F (B)$
13	3 7	jca	$⊢ (A \in V \land B \in W \land A \neq B) \to (A \in \{A, B\} \land B \in \{A, B\})$
14		f1veqaeq	$⊢ (F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \land (A \in \{A, B\} \land B \in \{A, B\})) \to (F (A) = F (B) \to A = B)$
15	13 14	sylan2	$⊢ (F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \land (A \in V \land B \in W \land A \neq B)) \to (F (A) = F (B) \to A = B)$
16	12 15	syl5	$⊢ (F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \land (A \in V \land B \in W \land A \neq B)) \to ((F (A) = X \land F (B) = X) \to A = B)$
17	16	ex	$⊢ F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \to ((A \in V \land B \in W \land A \neq B) \to ((F (A) = X \land F (B) = X) \to A = B))$
18		eqneqall	$⊢ A = B \to (A \neq B \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
19	18	com12	$⊢ A \neq B \to (A = B \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
20	19	3ad2ant3	$⊢ (A \in V \land B \in W \land A \neq B) \to (A = B \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
21	20	a1i	$⊢ F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \to ((A \in V \land B \in W \land A \neq B) \to (A = B \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X))))$
22	17 21	syldd	$⊢ F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \to ((A \in V \land B \in W \land A \neq B) \to ((F (A) = X \land F (B) = X) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X))))$
23	22	impcom	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to ((F (A) = X \land F (B) = X) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
24		olc	$⊢ (F (A) = Y \land F (B) = X) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X))$
25	24	a1i	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to ((F (A) = Y \land F (B) = X) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
26		orc	$⊢ (F (A) = X \land F (B) = Y) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X))$
27	26	a1i	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to ((F (A) = X \land F (B) = Y) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
28		eqtr3	$⊢ (F (A) = Y \land F (B) = Y) \to F (A) = F (B)$
29	28 15	syl5	$⊢ (F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \land (A \in V \land B \in W \land A \neq B)) \to ((F (A) = Y \land F (B) = Y) \to A = B)$
30	29	ex	$⊢ F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \to ((A \in V \land B \in W \land A \neq B) \to ((F (A) = Y \land F (B) = Y) \to A = B))$
31	30 21	syldd	$⊢ F : \{A, B\} \underset{1-1}{⟶} \{X, Y\} \to ((A \in V \land B \in W \land A \neq B) \to ((F (A) = Y \land F (B) = Y) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X))))$
32	31	impcom	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to ((F (A) = Y \land F (B) = Y) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
33	23 25 27 32	ccased	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to (((F (A) = X \lor F (A) = Y) \land (F (B) = X \lor F (B) = Y)) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
34	10 11 33	syl2ani	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to ((F (A) \in \{X, Y\} \land F (B) \in \{X, Y\}) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X)))$
35	5 9 34	mp2and	$⊢ ((A \in V \land B \in W \land A \neq B) \land F : \{A, B\} \underset{1-1}{⟶} \{X, Y\}) \to ((F (A) = X \land F (B) = Y) \lor (F (A) = Y \land F (B) = X))$

Metamath Proof Explorer

Theorem fvf1pr

Proof