Theorem 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 -> ( A e. Fin <-> ( dom A e. Fin /\ ran A e. Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmfi	|- ( A e. Fin -> dom A e. Fin )
2		rnfi	|- ( A e. Fin -> ran A e. Fin )
3	1 2	jca	|- ( A e. Fin -> ( dom A e. Fin /\ ran A e. Fin ) )
4		xpfi	|- ( ( dom A e. Fin /\ ran A e. Fin ) -> ( dom A X. ran A ) e. Fin )
5		relssdmrn	|- ( Rel A -> A C_ ( dom A X. ran A ) )
6		ssfi	|- ( ( ( dom A X. ran A ) e. Fin /\ A C_ ( dom A X. ran A ) ) -> A e. Fin )
7	4 5 6	syl2anr	|- ( ( Rel A /\ ( dom A e. Fin /\ ran A e. Fin ) ) -> A e. Fin )
8	7	ex	|- ( Rel A -> ( ( dom A e. Fin /\ ran A e. Fin ) -> A e. Fin ) )
9	3 8	impbid2	|- ( Rel A -> ( A e. Fin <-> ( dom A e. Fin /\ ran A e. Fin ) ) )