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) Avoid ax-pow . (Revised by BTernaryTau, 4-Jan-2025)

		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		php3	$⊢ (B \in Fin \land ran F \subset B) \to ran F ≺ B$
11	10	ex	$⊢ B \in Fin \to (ran F \subset B \to ran F ≺ B)$
12	11	ad2antlr	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F \subset B \to ran F ≺ B)$
13		enfii	$⊢ (B \in Fin \land A \approx B) \to A \in Fin$
14	13	ancoms	$⊢ (A \approx B \land B \in Fin) \to A \in Fin$
15		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
16		f1oenfi	$⊢ (A \in Fin \land F : A \underset{1-1 onto}{⟶} ran F) \to A \approx ran F$
17	14 15 16	syl2an	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to A \approx ran F$
18		endom	$⊢ A \approx ran F \to A ≼ ran F$
19		domsdomtrfi	$⊢ (A \in Fin \land A ≼ ran F \land ran F ≺ B) \to A ≺ B$
20	18 19	syl3an2	$⊢ (A \in Fin \land A \approx ran F \land ran F ≺ B) \to A ≺ B$
21	20	3expia	$⊢ (A \in Fin \land A \approx ran F) \to (ran F ≺ B \to A ≺ B)$
22	14 17 21	syl2an2r	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F ≺ B \to A ≺ B)$
23	12 22	syld	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (ran F \subset B \to A ≺ B)$
24		sdomnen	$⊢ A ≺ B \to \neg A \approx B$
25	23 24	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)$
26	9 25	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)$
27	26	necon4ad	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to (A \approx B \to ran F = B)$
28	5 27	mpd	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to ran F = B$
29		df-fo	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B)$
30	4 28 29	sylanbrc	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F : A \underset{onto}{⟶} B$
31		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
32	1 30 31	sylanbrc	$⊢ ((A \approx B \land B \in Fin) \land F : A \underset{1-1}{⟶} B) \to F : A \underset{1-1 onto}{⟶} B$
33	32	ex	$⊢ (A \approx B \land B \in Fin) \to (F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} B)$
34		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{1-1}{⟶} B$
35	33 34	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