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

Metamath Proof Explorer

Theorem funisfsupp

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

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

Proof

Step Hyp Ref Expression
1 isfsupp ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
2 1 3adant1 ⊢ ( ( Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
3 ibar ⊢ ( Fun 𝑅 → ( ( 𝑅 supp 𝑍 ) ∈ Fin ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
4 3 bicomd ⊢ ( Fun 𝑅 → ( ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )
5 4 3ad2ant1 ⊢ ( ( Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )
6 2 5 bitrd ⊢ ( ( Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )