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

Metamath Proof Explorer

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