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 | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1ofn | ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 Fn 𝐴 ) | |
| 2 | fnfi | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐹 ∈ Fin ) | |
| 3 | 1 2 | sylan | ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ Fin ) → 𝐹 ∈ Fin ) |
| 4 | 3 | ancoms | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐹 ∈ Fin ) |
| 5 | f1oen3g | ⊢ ( ( 𝐹 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 ) | |
| 6 | 4 5 | sylancom | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 ) |