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