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→ 𝐵 ) → 𝐴 ≈ 𝐵 )