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

Metamath Proof Explorer

Theorem isfsupp

Description: The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019)

Ref Expression
Assertion isfsupp ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 funeq ⊢ ( 𝑟 = 𝑅 → ( Fun 𝑟 ↔ Fun 𝑅 ) )
2 1 adantr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑧 = 𝑍 ) → ( Fun 𝑟 ↔ Fun 𝑅 ) )
3 oveq12 ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑧 = 𝑍 ) → ( 𝑟 supp 𝑧 ) = ( 𝑅 supp 𝑍 ) )
4 3 eleq1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑧 = 𝑍 ) → ( ( 𝑟 supp 𝑧 ) ∈ Fin ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )
5 2 4 anbi12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑧 = 𝑍 ) → ( ( Fun 𝑟 ∧ ( 𝑟 supp 𝑧 ) ∈ Fin ) ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
6 df-fsupp ⊢ finSupp = { ⟨ 𝑟 , 𝑧 ⟩ ∣ ( Fun 𝑟 ∧ ( 𝑟 supp 𝑧 ) ∈ Fin ) }
7 5 6 brabga ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )