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

Metamath Proof Explorer

Theorem fcdmnn0fsuppg

Description: Version of fcdmnn0fsupp avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 5-Aug-2024)

Ref Expression
Assertion fcdmnn0fsuppg ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 ffun ⊢ ( 𝐹 : 𝐼 ⟶ ℕ0 → Fun 𝐹 )
2 simpl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → 𝐹 ∈ 𝑉 )
3 c0ex ⊢ 0 ∈ V
4 funisfsupp ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
5 3 4 mp3an3 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
6 1 2 5 syl2an2 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
7 fcdmnn0suppg ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) )
8 7 eleq1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( ( 𝐹 supp 0 ) ∈ Fin ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
9 6 8 bitrd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )