Metamath Proof Explorer

Theorem hashrabsn01

Description: The size of a restricted class abstraction restricted to a singleton is either 0 or 1. (Contributed by Alexander van der Vekens, 3-Sep-2018)

Ref Expression
Assertion hashrabsn01 
|- ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) )

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 fveqeq2 
 |-  ( { x e. { A } | ph } = (/) -> ( ( # ` { x e. { A } | ph } ) = N <-> ( # ` (/) ) = N ) )
4 eqcom 
 |-  ( ( # ` (/) ) = N <-> N = ( # ` (/) ) )
5 4 biimpi 
 |-  ( ( # ` (/) ) = N -> N = ( # ` (/) ) )
6 hash0 
 |-  ( # ` (/) ) = 0
7 5 6 eqtrdi 
 |-  ( ( # ` (/) ) = N -> N = 0 )
8 7 orcd 
 |-  ( ( # ` (/) ) = N -> ( N = 0 \/ N = 1 ) )
9 3 8 biimtrdi 
 |-  ( { x e. { A } | ph } = (/) -> ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) ) )
10 fveqeq2 
 |-  ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = N <-> ( # ` { A } ) = N ) )
11 eqcom 
 |-  ( ( # ` { A } ) = N <-> N = ( # ` { A } ) )
12 11 biimpi 
 |-  ( ( # ` { A } ) = N -> N = ( # ` { A } ) )
13 hashsng 
 |-  ( A e. _V -> ( # ` { A } ) = 1 )
14 12 13 sylan9eqr 
 |-  ( ( A e. _V /\ ( # ` { A } ) = N ) -> N = 1 )
15 14 olcd 
 |-  ( ( A e. _V /\ ( # ` { A } ) = N ) -> ( N = 0 \/ N = 1 ) )
16 15 ex 
 |-  ( A e. _V -> ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) ) )
17 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
18 fveqeq2 
 |-  ( { A } = (/) -> ( ( # ` { A } ) = N <-> ( # ` (/) ) = N ) )
19 18 8 biimtrdi 
 |-  ( { A } = (/) -> ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) ) )
20 17 19 sylbi 
 |-  ( -. A e. _V -> ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) ) )
21 16 20 pm2.61i 
 |-  ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) )
22 10 21 biimtrdi 
 |-  ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) ) )
23 9 22 jaoi 
 |-  ( ( { x e. { A } | ph } = (/) \/ { x e. { A } | ph } = { A } ) -> ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) ) )
24 1 2 23 mp2b 
 |-  ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) )