relfi

Description: A relation (set) is finite if and only if both its domain and range are finite. (Contributed by Thierry Arnoux, 27-Aug-2017)

		Ref	Expression
	Assertion	relfi	$⊢ Rel A \to (A \in Fin \leftrightarrow (dom A \in Fin \land ran A \in Fin))$

Step	Hyp	Ref	Expression
1		dmfi	$⊢ A \in Fin \to dom A \in Fin$
2		rnfi	$⊢ A \in Fin \to ran A \in Fin$
3	1 2	jca	$⊢ A \in Fin \to (dom A \in Fin \land ran A \in Fin)$
4		xpfi	$⊢ (dom A \in Fin \land ran A \in Fin) \to dom A \times ran A \in Fin$
5		relssdmrn	$⊢ Rel A \to A \subseteq dom A \times ran A$
6		ssfi	$⊢ (dom A \times ran A \in Fin \land A \subseteq dom A \times ran A) \to A \in Fin$
7	4 5 6	syl2anr	$⊢ (Rel A \land (dom A \in Fin \land ran A \in Fin)) \to A \in Fin$
8	7	ex	$⊢ Rel A \to ((dom A \in Fin \land ran A \in Fin) \to A \in Fin)$
9	3 8	impbid2	$⊢ Rel A \to (A \in Fin \leftrightarrow (dom A \in Fin \land ran A \in Fin))$

Metamath Proof Explorer