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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion snifpsrbag ( ( 𝐼 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 𝑁 , 0 ) ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ) ) ∈ 𝐷 )