Theorem relfsupp 9303

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

Assertion

Ref	Expression
relfsupp	⊢ Rel finSupp

Proof of Theorem relfsupp

Dummy variables 𝑧 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fsupp 9302	. 2 ⊢ finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
2	1	relopabiv 5789	1 ⊢ Rel finSupp

Syntax hints:   ∧ wa 399   ∈ wcel 2141  Rel wrel 5648  Fun wfun 6510  (class class class)co 7391   supp csupp 8134  Fincfn 8921   finSupp cfsupp 9301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-opab 5160  df-xp 5649  df-rel 5650  df-fsupp 9302

This theorem is referenced by:  relprcnfsupp  9304  fsuppimp  9308  suppeqfsuppbi  9319  fsuppsssupp  9321  fsuppss  9323  fsuppssov1  9324  fsuppunbi  9329  funsnfsupp  9332  wemapso2  9495  gsumhashmul  33208