f1finf1o

Description: Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010) (Revised by Mario Carneiro, 27-Feb-2014)

		Ref	Expression
	Assertion	f1finf1o	$⊢ (A \approx B \land B \in Fin) \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : A \underset{1-1 onto}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F : A \underset{1-1}{⟶} B$
2		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
3	2	adantl	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F : A ⟶ B$
4	3	ffnd	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F Fn A$
5		simpll	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to A \approx B$
6	3	frnd	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to ran F \subseteq B$
7		df-pss	$⊢ ran F \subset B \leftrightarrow (ran F \subseteq B \land ran F \neq B)$
8	7	baib	$⊢ ran F \subseteq B \to (ran F \subset B \leftrightarrow ran F \neq B)$
9	6 8	syl	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F \subset B \leftrightarrow ran F \neq B)$
10		simplr	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to B \in Fin$
11		relen	$⊢ Rel \approx$
12	11	brrelex1i	$⊢ A \approx B \to A \in V$
13	5 12	syl	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to A \in V$
14	10 13	elmapd	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (F \in (B^{A}) \leftrightarrow F : A ⟶ B)$
15	3 14	mpbird	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F \in (B^{A})$
16		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
17	16	adantl	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F : A \underset{1-1 onto}{⟶} ran F$
18		f1oen3g	$⊢ (F \in (B^{A}) \land F : A \underset{1-1 onto}{⟶} ran F) \to A \approx ran F$
19	15 17 18	syl2anc	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to A \approx ran F$
20		php3	$⊢ (B \in Fin \land ran F \subset B) \to ran F ≺ B$
21	20	ex	$⊢ B \in Fin \to (ran F \subset B \to ran F ≺ B)$
22	10 21	syl	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F \subset B \to ran F ≺ B)$
23		ensdomtr	$⊢ (A \approx ran F \land ran F ≺ B) \to A ≺ B$
24	19 22 23	syl6an	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F \subset B \to A ≺ B)$
25		sdomnen	$⊢ A ≺ B \to \neg A \approx B$
26	24 25	syl6	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F \subset B \to \neg A \approx B)$
27	9 26	sylbird	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F \neq B \to \neg A \approx B)$
28	27	necon4ad	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (A \approx B \to ran F = B)$
29	5 28	mpd	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to ran F = B$
30		df-fo	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B)$
31	4 29 30	sylanbrc	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F : A \underset{onto}{⟶} B$
32		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
33	1 31 32	sylanbrc	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F : A \underset{1-1 onto}{⟶} B$
34	33	ex	$⊢ (A \approx B \land B \in Fin) \to (F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} B)$
35		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{1-1}{⟶} B$
36	34 35	impbid1	$⊢ (A \approx B \land B \in Fin) \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : A \underset{1-1 onto}{⟶} B)$

Metamath Proof Explorer

Theorem f1finf1o

Proof