This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 ) ) )