Theorem f1vrnfibi

Description: A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi . (Contributed by AV, 10-Jan-2020)

	Ref	Expression
Assertion	f1vrnfibi	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		f1dm	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → dom 𝐹 = 𝐴 )
2		dmexg	⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
3		eleq1	⊢ ( 𝐴 = dom 𝐹 → ( 𝐴 ∈ V ↔ dom 𝐹 ∈ V ) )
4	3	eqcoms	⊢ ( dom 𝐹 = 𝐴 → ( 𝐴 ∈ V ↔ dom 𝐹 ∈ V ) )
5	2 4	imbitrrid	⊢ ( dom 𝐹 = 𝐴 → ( 𝐹 ∈ 𝑉 → 𝐴 ∈ V ) )
6	1 5	syl	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐹 ∈ 𝑉 → 𝐴 ∈ V ) )
7	6	impcom	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ∈ V )
8		f1dmvrnfibi	⊢ ( ( 𝐴 ∈ V ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )
9	7 8	sylancom	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )