This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrbagsn

Description: A singleton bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypothesis psrbag0.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbagsn 
|- ( I e. V -> ( x e. I |-> if ( x = K , 1 , 0 ) ) e. D )

Proof

Step Hyp Ref Expression
1 psrbag0.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 1nn0 
 |-  1 e. NN0
3 0nn0 
 |-  0 e. NN0
4 2 3 ifcli 
 |-  if ( x = K , 1 , 0 ) e. NN0
5 4 a1i 
 |-  ( ( T. /\ x e. I ) -> if ( x = K , 1 , 0 ) e. NN0 )
6 5 fmpttd 
 |-  ( T. -> ( x e. I |-> if ( x = K , 1 , 0 ) ) : I --> NN0 )
7 6 mptru 
 |-  ( x e. I |-> if ( x = K , 1 , 0 ) ) : I --> NN0
8 eqid 
 |-  ( x e. I |-> if ( x = K , 1 , 0 ) ) = ( x e. I |-> if ( x = K , 1 , 0 ) )
9 8 mptpreima 
 |-  ( `' ( x e. I |-> if ( x = K , 1 , 0 ) ) " NN ) = { x e. I | if ( x = K , 1 , 0 ) e. NN }
10 snfi 
 |-  { K } e. Fin
11 inss1 
 |-  ( { x | x = K } i^i I ) C_ { x | x = K }
12 dfrab2 
 |-  { x e. I | x = K } = ( { x | x = K } i^i I )
13 df-sn 
 |-  { K } = { x | x = K }
14 11 12 13 3sstr4i 
 |-  { x e. I | x = K } C_ { K }
15 ssfi 
 |-  ( ( { K } e. Fin /\ { x e. I | x = K } C_ { K } ) -> { x e. I | x = K } e. Fin )
16 10 14 15 mp2an 
 |-  { x e. I | x = K } e. Fin
17 0nnn 
 |-  -. 0 e. NN
18 iffalse 
 |-  ( -. x = K -> if ( x = K , 1 , 0 ) = 0 )
19 18 eleq1d 
 |-  ( -. x = K -> ( if ( x = K , 1 , 0 ) e. NN <-> 0 e. NN ) )
20 17 19 mtbiri 
 |-  ( -. x = K -> -. if ( x = K , 1 , 0 ) e. NN )
21 20 con4i 
 |-  ( if ( x = K , 1 , 0 ) e. NN -> x = K )
22 21 a1i 
 |-  ( x e. I -> ( if ( x = K , 1 , 0 ) e. NN -> x = K ) )
23 22 ss2rabi 
 |-  { x e. I | if ( x = K , 1 , 0 ) e. NN } C_ { x e. I | x = K }
24 ssfi 
 |-  ( ( { x e. I | x = K } e. Fin /\ { x e. I | if ( x = K , 1 , 0 ) e. NN } C_ { x e. I | x = K } ) -> { x e. I | if ( x = K , 1 , 0 ) e. NN } e. Fin )
25 16 23 24 mp2an 
 |-  { x e. I | if ( x = K , 1 , 0 ) e. NN } e. Fin
26 9 25 eqeltri 
 |-  ( `' ( x e. I |-> if ( x = K , 1 , 0 ) ) " NN ) e. Fin
27 7 26 pm3.2i 
 |-  ( ( x e. I |-> if ( x = K , 1 , 0 ) ) : I --> NN0 /\ ( `' ( x e. I |-> if ( x = K , 1 , 0 ) ) " NN ) e. Fin )
28 1 psrbag 
 |-  ( I e. V -> ( ( x e. I |-> if ( x = K , 1 , 0 ) ) e. D <-> ( ( x e. I |-> if ( x = K , 1 , 0 ) ) : I --> NN0 /\ ( `' ( x e. I |-> if ( x = K , 1 , 0 ) ) " NN ) e. Fin ) ) )
29 27 28 mpbiri 
 |-  ( I e. V -> ( x e. I |-> if ( x = K , 1 , 0 ) ) e. D )