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 syl6bi
 |-  ( { 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 syl6bi
 |-  ( { 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 syl6bi
 |-  ( { 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 ) )