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 Fin F : A 1-1 onto B A B

Proof

Step Hyp Ref Expression
1 f1ofn F : A 1-1 onto B F Fn A
2 fnfi F Fn A A Fin F Fin
3 1 2 sylan F : A 1-1 onto B A Fin F Fin
4 3 ancoms A Fin F : A 1-1 onto B F Fin
5 f1oen3g F Fin F : A 1-1 onto B A B
6 4 5 sylancom A Fin F : A 1-1 onto B A B