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

Metamath Proof Explorer

Theorem psrbag0

Description: The empty 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 psrbag0 
|- ( I e. V -> ( I X. { 0 } ) e. D )

Proof

Step Hyp Ref Expression
1 psrbag0.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 0nn0 
 |-  0 e. NN0
3 2 fconst6 
 |-  ( I X. { 0 } ) : I --> NN0
4 c0ex 
 |-  0 e. _V
5 4 fconst 
 |-  ( I X. { 0 } ) : I --> { 0 }
6 incom 
 |-  ( { 0 } i^i NN ) = ( NN i^i { 0 } )
7 0nnn 
 |-  -. 0 e. NN
8 disjsn 
 |-  ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
9 7 8 mpbir 
 |-  ( NN i^i { 0 } ) = (/)
10 6 9 eqtri 
 |-  ( { 0 } i^i NN ) = (/)
11 fimacnvdisj 
 |-  ( ( ( I X. { 0 } ) : I --> { 0 } /\ ( { 0 } i^i NN ) = (/) ) -> ( `' ( I X. { 0 } ) " NN ) = (/) )
12 5 10 11 mp2an 
 |-  ( `' ( I X. { 0 } ) " NN ) = (/)
13 0fi 
 |-  (/) e. Fin
14 12 13 eqeltri 
 |-  ( `' ( I X. { 0 } ) " NN ) e. Fin
15 3 14 pm3.2i 
 |-  ( ( I X. { 0 } ) : I --> NN0 /\ ( `' ( I X. { 0 } ) " NN ) e. Fin )
16 1 psrbag 
 |-  ( I e. V -> ( ( I X. { 0 } ) e. D <-> ( ( I X. { 0 } ) : I --> NN0 /\ ( `' ( I X. { 0 } ) " NN ) e. Fin ) ) )
17 15 16 mpbiri 
 |-  ( I e. V -> ( I X. { 0 } ) e. D )