Metamath Proof Explorer


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 RelAAFindomAFinranAFin

Proof

Step Hyp Ref Expression
1 dmfi AFindomAFin
2 rnfi AFinranAFin
3 1 2 jca AFindomAFinranAFin
4 xpfi domAFinranAFindomA×ranAFin
5 relssdmrn RelAAdomA×ranA
6 ssfi domA×ranAFinAdomA×ranAAFin
7 4 5 6 syl2anr RelAdomAFinranAFinAFin
8 7 ex RelAdomAFinranAFinAFin
9 3 8 impbid2 RelAAFindomAFinranAFin