Theorem hashrabrsn

Description: The size of a restricted class abstraction restricted to a singleton is a nonnegative integer. (Contributed by Alexander van der Vekens, 22-Dec-2017)

	Ref	Expression
Assertion	hashrabrsn	|- ( # ` { x e. { A } | ph } ) e. NN0

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { x e. { A } | ph } = { x e. { A } | ph }
2		rabrsn	|- ( { x e. { A } | ph } = { x e. { A } | ph } -> ( { x e. { A } | ph } = (/) \/ { x e. { A } | ph } = { A } ) )
3		fveq2	|- ( { x e. { A } | ph } = (/) -> ( # ` { x e. { A } | ph } ) = ( # ` (/) ) )
4		hash0	|- ( # ` (/) ) = 0
5		0nn0	|- 0 e. NN0
6	4 5	eqeltri	|- ( # ` (/) ) e. NN0
7	3 6	eqeltrdi	|- ( { x e. { A } | ph } = (/) -> ( # ` { x e. { A } | ph } ) e. NN0 )
8		fveq2	|- ( { x e. { A } | ph } = { A } -> ( # ` { x e. { A } | ph } ) = ( # ` { A } ) )
9		hashsng	|- ( A e. _V -> ( # ` { A } ) = 1 )
10		1nn0	|- 1 e. NN0
11	9 10	eqeltrdi	|- ( A e. _V -> ( # ` { A } ) e. NN0 )
12		snprc	|- ( -. A e. _V <-> { A } = (/) )
13		fveq2	|- ( { A } = (/) -> ( # ` { A } ) = ( # ` (/) ) )
14	13 6	eqeltrdi	|- ( { A } = (/) -> ( # ` { A } ) e. NN0 )
15	12 14	sylbi	|- ( -. A e. _V -> ( # ` { A } ) e. NN0 )
16	11 15	pm2.61i	|- ( # ` { A } ) e. NN0
17	8 16	eqeltrdi	|- ( { x e. { A } | ph } = { A } -> ( # ` { x e. { A } | ph } ) e. NN0 )
18	7 17	jaoi	|- ( ( { x e. { A } | ph } = (/) \/ { x e. { A } | ph } = { A } ) -> ( # ` { x e. { A } | ph } ) e. NN0 )
19	1 2 18	mp2b	|- ( # ` { x e. { A } | ph } ) e. NN0