This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
2 f1ofn ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 Fn 𝐵 )
3 fnfi ⊢ ( ( ◡ 𝐹 Fn 𝐵 ∧ 𝐵 ∈ Fin ) → ◡ 𝐹 ∈ Fin )
4 2 3 sylan ⊢ ( ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐵 ∈ Fin ) → ◡ 𝐹 ∈ Fin )
5 1 4 sylan ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ Fin ) → ◡ 𝐹 ∈ Fin )
6 5 ancoms ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → ◡ 𝐹 ∈ Fin )
7 cnvfi ⊢ ( ◡ 𝐹 ∈ Fin → ◡ ◡ 𝐹 ∈ Fin )
8 f1orel ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐹 )
9 dfrel2 ⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
10 8 9 sylib ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ ◡ 𝐹 = 𝐹 )
11 10 eleq1d ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ ◡ 𝐹 ∈ Fin ↔ 𝐹 ∈ Fin ) )
12 11 biimpac ⊢ ( ( ◡ ◡ 𝐹 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐹 ∈ Fin )
13 7 12 sylan ⊢ ( ( ◡ 𝐹 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐹 ∈ Fin )
14 6 13 sylancom ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐹 ∈ Fin )
15 f1oen3g ⊢ ( ( 𝐹 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )
16 14 15 sylancom ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )