# Metamath Proof Explorer

## Theorem 0hashbc

Description: There are no subsets of the empty set with size greater than zero. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypothesis ramval.c
`|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
Assertion 0hashbc
`|- ( N e. NN -> ( (/) C N ) = (/) )`

### Proof

Step Hyp Ref Expression
1 ramval.c
` |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
2 0fin
` |-  (/) e. Fin`
3 nnnn0
` |-  ( N e. NN -> N e. NN0 )`
4 1 hashbc2
` |-  ( ( (/) e. Fin /\ N e. NN0 ) -> ( # ` ( (/) C N ) ) = ( ( # ` (/) ) _C N ) )`
5 2 3 4 sylancr
` |-  ( N e. NN -> ( # ` ( (/) C N ) ) = ( ( # ` (/) ) _C N ) )`
6 hash0
` |-  ( # ` (/) ) = 0`
7 6 oveq1i
` |-  ( ( # ` (/) ) _C N ) = ( 0 _C N )`
8 bc0k
` |-  ( N e. NN -> ( 0 _C N ) = 0 )`
9 7 8 syl5eq
` |-  ( N e. NN -> ( ( # ` (/) ) _C N ) = 0 )`
10 5 9 eqtrd
` |-  ( N e. NN -> ( # ` ( (/) C N ) ) = 0 )`
11 ovex
` |-  ( (/) C N ) e. _V`
12 hasheq0
` |-  ( ( (/) C N ) e. _V -> ( ( # ` ( (/) C N ) ) = 0 <-> ( (/) C N ) = (/) ) )`
13 11 12 ax-mp
` |-  ( ( # ` ( (/) C N ) ) = 0 <-> ( (/) C N ) = (/) )`
14 10 13 sylib
` |-  ( N e. NN -> ( (/) C N ) = (/) )`