Metamath Proof Explorer

Theorem f1oenfirn

Description: If the range of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. (Contributed by BTernaryTau, 9-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1 onto}{⟶} A$
2		f1ofn	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} Fn B$
3		fnfi	$⊢ (F^{-1} Fn B \land B \in Fin) \to F^{-1} \in Fin$
4	2 3	sylan	$⊢ (F^{-1} : B \underset{1-1 onto}{⟶} A \land B \in Fin) \to F^{-1} \in Fin$
5	1 4	sylan	$⊢ (F : A \underset{1-1 onto}{⟶} B \land B \in Fin) \to F^{-1} \in Fin$
6	5	ancoms	$⊢ (B \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to F^{-1} \in Fin$
7		cnvfi	$⊢ F^{-1} \in Fin \to {F^{-1}}^{-1} \in Fin$
8		f1orel	$⊢ F : A \underset{1-1 onto}{⟶} B \to Rel F$
9		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
10	8 9	sylib	$⊢ F : A \underset{1-1 onto}{⟶} B \to {F^{-1}}^{-1} = F$
11	10	eleq1d	$⊢ F : A \underset{1-1 onto}{⟶} B \to ({F^{-1}}^{-1} \in Fin \leftrightarrow F \in Fin)$
12	11	biimpac	$⊢ ({F^{-1}}^{-1} \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to F \in Fin$
13	7 12	sylan	$⊢ (F^{-1} \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to F \in Fin$
14	6 13	sylancom	$⊢ (B \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to F \in Fin$
15		f1oen3g	$⊢ (F \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to A \approx B$
16	14 15	sylancom	$⊢ (B \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to A \approx B$