Metamath Proof Explorer


Theorem snifpsrbag

Description: A bag containing one element is a finite bag. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by AV, 8-Jul-2019)

Ref Expression
Hypothesis psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion snifpsrbag ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 simpr ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
3 0nn0 0 ∈ ℕ0
4 3 a1i ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → 0 ∈ ℕ0 )
5 2 4 ifcld ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ∈ ℕ0 )
6 5 adantr ( ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) ∧ 𝑦𝐼 ) → if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ∈ ℕ0 )
7 6 fmpttd ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) : 𝐼 ⟶ ℕ0 )
8 id ( 𝐼𝑉𝐼𝑉 )
9 c0ex 0 ∈ V
10 9 a1i ( 𝐼𝑉 → 0 ∈ V )
11 eqid ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) )
12 8 10 11 sniffsupp ( 𝐼𝑉 → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) finSupp 0 )
13 12 adantr ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) finSupp 0 )
14 frnnn0fsupp ( ( 𝐼𝑉 ∧ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) : 𝐼 ⟶ ℕ0 ) → ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) finSupp 0 ↔ ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) “ ℕ ) ∈ Fin ) )
15 14 adantlr ( ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) ∧ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) : 𝐼 ⟶ ℕ0 ) → ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) finSupp 0 ↔ ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) “ ℕ ) ∈ Fin ) )
16 15 bicomd ( ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) ∧ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) : 𝐼 ⟶ ℕ0 ) → ( ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) “ ℕ ) ∈ Fin ↔ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) finSupp 0 ) )
17 7 16 mpdan ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → ( ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) “ ℕ ) ∈ Fin ↔ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) finSupp 0 ) )
18 13 17 mpbird ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) “ ℕ ) ∈ Fin )
19 1 psrbag ( 𝐼𝑉 → ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) “ ℕ ) ∈ Fin ) ) )
20 19 adantr ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) “ ℕ ) ∈ Fin ) ) )
21 7 18 20 mpbir2and ( ( 𝐼𝑉𝑁 ∈ ℕ0 ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) ∈ 𝐷 )