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 e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion snifpsrbag 
|- ( ( I e. V /\ N e. NN0 ) -> ( y e. I |-> if ( y = X , N , 0 ) ) e. D )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 simpr 
 |-  ( ( I e. V /\ N e. NN0 ) -> N e. NN0 )
3 0nn0 
 |-  0 e. NN0
4 3 a1i 
 |-  ( ( I e. V /\ N e. NN0 ) -> 0 e. NN0 )
5 2 4 ifcld 
 |-  ( ( I e. V /\ N e. NN0 ) -> if ( y = X , N , 0 ) e. NN0 )
6 5 adantr 
 |-  ( ( ( I e. V /\ N e. NN0 ) /\ y e. I ) -> if ( y = X , N , 0 ) e. NN0 )
7 6 fmpttd 
 |-  ( ( I e. V /\ N e. NN0 ) -> ( y e. I |-> if ( y = X , N , 0 ) ) : I --> NN0 )
8 id 
 |-  ( I e. V -> I e. V )
9 c0ex 
 |-  0 e. _V
10 9 a1i 
 |-  ( I e. V -> 0 e. _V )
11 eqid 
 |-  ( y e. I |-> if ( y = X , N , 0 ) ) = ( y e. I |-> if ( y = X , N , 0 ) )
12 8 10 11 sniffsupp 
 |-  ( I e. V -> ( y e. I |-> if ( y = X , N , 0 ) ) finSupp 0 )
13 12 adantr 
 |-  ( ( I e. V /\ N e. NN0 ) -> ( y e. I |-> if ( y = X , N , 0 ) ) finSupp 0 )
14 frnnn0fsupp 
 |-  ( ( I e. V /\ ( y e. I |-> if ( y = X , N , 0 ) ) : I --> NN0 ) -> ( ( y e. I |-> if ( y = X , N , 0 ) ) finSupp 0 <-> ( `' ( y e. I |-> if ( y = X , N , 0 ) ) " NN ) e. Fin ) )
15 14 adantlr 
 |-  ( ( ( I e. V /\ N e. NN0 ) /\ ( y e. I |-> if ( y = X , N , 0 ) ) : I --> NN0 ) -> ( ( y e. I |-> if ( y = X , N , 0 ) ) finSupp 0 <-> ( `' ( y e. I |-> if ( y = X , N , 0 ) ) " NN ) e. Fin ) )
16 15 bicomd 
 |-  ( ( ( I e. V /\ N e. NN0 ) /\ ( y e. I |-> if ( y = X , N , 0 ) ) : I --> NN0 ) -> ( ( `' ( y e. I |-> if ( y = X , N , 0 ) ) " NN ) e. Fin <-> ( y e. I |-> if ( y = X , N , 0 ) ) finSupp 0 ) )
17 7 16 mpdan 
 |-  ( ( I e. V /\ N e. NN0 ) -> ( ( `' ( y e. I |-> if ( y = X , N , 0 ) ) " NN ) e. Fin <-> ( y e. I |-> if ( y = X , N , 0 ) ) finSupp 0 ) )
18 13 17 mpbird 
 |-  ( ( I e. V /\ N e. NN0 ) -> ( `' ( y e. I |-> if ( y = X , N , 0 ) ) " NN ) e. Fin )
19 1 psrbag 
 |-  ( I e. V -> ( ( y e. I |-> if ( y = X , N , 0 ) ) e. D <-> ( ( y e. I |-> if ( y = X , N , 0 ) ) : I --> NN0 /\ ( `' ( y e. I |-> if ( y = X , N , 0 ) ) " NN ) e. Fin ) ) )
20 19 adantr 
 |-  ( ( I e. V /\ N e. NN0 ) -> ( ( y e. I |-> if ( y = X , N , 0 ) ) e. D <-> ( ( y e. I |-> if ( y = X , N , 0 ) ) : I --> NN0 /\ ( `' ( y e. I |-> if ( y = X , N , 0 ) ) " NN ) e. Fin ) ) )
21 7 18 20 mpbir2and 
 |-  ( ( I e. V /\ N e. NN0 ) -> ( y e. I |-> if ( y = X , N , 0 ) ) e. D )