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	eqtrid	|- ( 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 ) = (/) )