# 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 $⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin$
Assertion snifpsrbag $⊢ I ∈ V ∧ N ∈ ℕ 0 → y ∈ I ⟼ if y = X N 0 ∈ D$

### Proof

Step Hyp Ref Expression
1 psrbag.d $⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin$
2 simpr $⊢ I ∈ V ∧ N ∈ ℕ 0 → N ∈ ℕ 0$
3 0nn0 $⊢ 0 ∈ ℕ 0$
4 3 a1i $⊢ I ∈ V ∧ N ∈ ℕ 0 → 0 ∈ ℕ 0$
5 2 4 ifcld $⊢ I ∈ V ∧ N ∈ ℕ 0 → if y = X N 0 ∈ ℕ 0$
6 5 adantr $⊢ I ∈ V ∧ N ∈ ℕ 0 ∧ y ∈ I → if y = X N 0 ∈ ℕ 0$
7 6 fmpttd $⊢ I ∈ V ∧ N ∈ ℕ 0 → y ∈ I ⟼ if y = X N 0 : I ⟶ ℕ 0$
8 id $⊢ I ∈ V → I ∈ V$
9 c0ex $⊢ 0 ∈ V$
10 9 a1i $⊢ I ∈ V → 0 ∈ V$
11 eqid $⊢ y ∈ I ⟼ if y = X N 0 = y ∈ I ⟼ if y = X N 0$
12 8 10 11 sniffsupp $⊢ I ∈ V → finSupp 0 ⁡ y ∈ I ⟼ if y = X N 0$
13 12 adantr $⊢ I ∈ V ∧ N ∈ ℕ 0 → finSupp 0 ⁡ y ∈ I ⟼ if y = X N 0$
14 frnnn0fsupp $⊢ I ∈ V ∧ y ∈ I ⟼ if y = X N 0 : I ⟶ ℕ 0 → finSupp 0 ⁡ y ∈ I ⟼ if y = X N 0 ↔ y ∈ I ⟼ if y = X N 0 -1 ℕ ∈ Fin$
15 14 adantlr $⊢ I ∈ V ∧ N ∈ ℕ 0 ∧ y ∈ I ⟼ if y = X N 0 : I ⟶ ℕ 0 → finSupp 0 ⁡ y ∈ I ⟼ if y = X N 0 ↔ y ∈ I ⟼ if y = X N 0 -1 ℕ ∈ Fin$
16 15 bicomd $⊢ I ∈ V ∧ N ∈ ℕ 0 ∧ y ∈ I ⟼ if y = X N 0 : I ⟶ ℕ 0 → y ∈ I ⟼ if y = X N 0 -1 ℕ ∈ Fin ↔ finSupp 0 ⁡ y ∈ I ⟼ if y = X N 0$
17 7 16 mpdan $⊢ I ∈ V ∧ N ∈ ℕ 0 → y ∈ I ⟼ if y = X N 0 -1 ℕ ∈ Fin ↔ finSupp 0 ⁡ y ∈ I ⟼ if y = X N 0$
18 13 17 mpbird $⊢ I ∈ V ∧ N ∈ ℕ 0 → y ∈ I ⟼ if y = X N 0 -1 ℕ ∈ Fin$
19 1 psrbag $⊢ I ∈ V → y ∈ I ⟼ if y = X N 0 ∈ D ↔ y ∈ I ⟼ if y = X N 0 : I ⟶ ℕ 0 ∧ y ∈ I ⟼ if y = X N 0 -1 ℕ ∈ Fin$
20 19 adantr $⊢ I ∈ V ∧ N ∈ ℕ 0 → y ∈ I ⟼ if y = X N 0 ∈ D ↔ y ∈ I ⟼ if y = X N 0 : I ⟶ ℕ 0 ∧ y ∈ I ⟼ if y = X N 0 -1 ℕ ∈ Fin$
21 7 18 20 mpbir2and $⊢ I ∈ V ∧ N ∈ ℕ 0 → y ∈ I ⟼ if y = X N 0 ∈ D$