Metamath Proof Explorer

Theorem relfsupp

Description: The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019)

Ref Expression
Assertion relfsupp 
|- Rel finSupp

Proof

Step Hyp Ref Expression
1 df-fsupp 
 |-  finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
2 1 relopabiv 
 |-  Rel finSupp