Metamath Proof Explorer

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	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to (F \in Fin \leftrightarrow ran F \in Fin)$

Proof

Step	Hyp	Ref	Expression
1		f1dm	$⊢ F : A \underset{1-1}{⟶} B \to dom F = A$
2		dmexg	$⊢ F \in V \to dom F \in V$
3		eleq1	$⊢ A = dom F \to (A \in V \leftrightarrow dom F \in V)$
4	3	eqcoms	$⊢ dom F = A \to (A \in V \leftrightarrow dom F \in V)$
5	2 4	imbitrrid	$⊢ dom F = A \to (F \in V \to A \in V)$
6	1 5	syl	$⊢ F : A \underset{1-1}{⟶} B \to (F \in V \to A \in V)$
7	6	impcom	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to A \in V$
8		f1dmvrnfibi	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (F \in Fin \leftrightarrow ran F \in Fin)$
9	7 8	sylancom	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to (F \in Fin \leftrightarrow ran F \in Fin)$