Metamath Proof Explorer

Theorem f1oenfi

Description: If the domain of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1oeng ). (Contributed by BTernaryTau, 8-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} B \to F Fn A$
2		fnfi	$⊢ (F Fn A \land A \in Fin) \to F \in Fin$
3	1 2	sylan	$⊢ (F : A \underset{1-1 onto}{⟶} B \land A \in Fin) \to F \in Fin$
4	3	ancoms	$⊢ (A \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to F \in Fin$
5		f1oen3g	$⊢ (F \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to A \approx B$
6	4 5	sylancom	$⊢ (A \in Fin \land F : A \underset{1-1 onto}{⟶} B) \to A \approx B$