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

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢D=f∈ℕ0I|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→ify=XN0∈ℕ0
6 5 adantr ⊢I∈V∧N∈ℕ0∧y∈I→ify=XN0∈ℕ0
7 6 fmpttd ⊢I∈V∧N∈ℕ0→y∈I⟼ify=XN0:I⟶ℕ0
8 id ⊢I∈V→I∈V
9 c0ex ⊢0∈V
10 9 a1i ⊢I∈V→0∈V
11 eqid ⊢y∈I⟼ify=XN0=y∈I⟼ify=XN0
12 8 10 11 sniffsupp ⊢I∈V→finSupp0⁡y∈I⟼ify=XN0
13 12 adantr ⊢I∈V∧N∈ℕ0→finSupp0⁡y∈I⟼ify=XN0
14 fcdmnn0fsupp ⊢I∈V∧y∈I⟼ify=XN0:I⟶ℕ0→finSupp0⁡y∈I⟼ify=XN0↔y∈I⟼ify=XN0-1ℕ∈Fin
15 14 adantlr ⊢I∈V∧N∈ℕ0∧y∈I⟼ify=XN0:I⟶ℕ0→finSupp0⁡y∈I⟼ify=XN0↔y∈I⟼ify=XN0-1ℕ∈Fin
16 15 bicomd ⊢I∈V∧N∈ℕ0∧y∈I⟼ify=XN0:I⟶ℕ0→y∈I⟼ify=XN0-1ℕ∈Fin↔finSupp0⁡y∈I⟼ify=XN0
17 7 16 mpdan ⊢I∈V∧N∈ℕ0→y∈I⟼ify=XN0-1ℕ∈Fin↔finSupp0⁡y∈I⟼ify=XN0
18 13 17 mpbird ⊢I∈V∧N∈ℕ0→y∈I⟼ify=XN0-1ℕ∈Fin
19 1 psrbag ⊢I∈V→y∈I⟼ify=XN0∈D↔y∈I⟼ify=XN0:I⟶ℕ0∧y∈I⟼ify=XN0-1ℕ∈Fin
20 19 adantr ⊢I∈V∧N∈ℕ0→y∈I⟼ify=XN0∈D↔y∈I⟼ify=XN0:I⟶ℕ0∧y∈I⟼ify=XN0-1ℕ∈Fin
21 7 18 20 mpbir2and ⊢I∈V∧N∈ℕ0→y∈I⟼ify=XN0∈D