f1dmvrnfibi

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

		Ref	Expression
	Assertion	f1dmvrnfibi	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (F \in Fin \leftrightarrow ran F \in Fin)$

Proof

Step	Hyp	Ref	Expression
1		rnfi	$⊢ F \in Fin \to ran F \in Fin$
2		simpr	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land ran F \in Fin) \to ran F \in Fin$
3		f1dm	$⊢ F : A \underset{1-1}{⟶} B \to dom F = A$
4		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
5		eleq1	$⊢ A = dom F \to (A \in V \leftrightarrow dom F \in V)$
6		f1oeq2	$⊢ A = dom F \to (F : A \underset{1-1 onto}{⟶} ran F \leftrightarrow F : dom F \underset{1-1 onto}{⟶} ran F)$
7	5 6	anbi12d	$⊢ A = dom F \to ((A \in V \land F : A \underset{1-1 onto}{⟶} ran F) \leftrightarrow (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F))$
8	7	eqcoms	$⊢ dom F = A \to ((A \in V \land F : A \underset{1-1 onto}{⟶} ran F) \leftrightarrow (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F))$
9	8	biimpd	$⊢ dom F = A \to ((A \in V \land F : A \underset{1-1 onto}{⟶} ran F) \to (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F))$
10	9	expcomd	$⊢ dom F = A \to (F : A \underset{1-1 onto}{⟶} ran F \to (A \in V \to (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F)))$
11	3 4 10	sylc	$⊢ F : A \underset{1-1}{⟶} B \to (A \in V \to (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F))$
12	11	impcom	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F)$
13	12	adantr	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land ran F \in Fin) \to (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F)$
14		f1oeng	$⊢ (dom F \in V \land F : dom F \underset{1-1 onto}{⟶} ran F) \to dom F \approx ran F$
15	13 14	syl	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land ran F \in Fin) \to dom F \approx ran F$
16		enfii	$⊢ (ran F \in Fin \land dom F \approx ran F) \to dom F \in Fin$
17	2 15 16	syl2anc	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land ran F \in Fin) \to dom F \in Fin$
18		f1fun	$⊢ F : A \underset{1-1}{⟶} B \to Fun F$
19	18	ad2antlr	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land ran F \in Fin) \to Fun F$
20		fundmfibi	$⊢ Fun F \to (F \in Fin \leftrightarrow dom F \in Fin)$
21	19 20	syl	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land ran F \in Fin) \to (F \in Fin \leftrightarrow dom F \in Fin)$
22	17 21	mpbird	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land ran F \in Fin) \to F \in Fin$
23	22	ex	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (ran F \in Fin \to F \in Fin)$
24	1 23	impbid2	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (F \in Fin \leftrightarrow ran F \in Fin)$

Metamath Proof Explorer

Theorem f1dmvrnfibi

Proof