Theorem hashsn01

Description: The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Assertion	hashsn01	|- ( ( # ` { A } ) = 0 \/ ( # ` { A } ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		hashsng	|- ( A e. _V -> ( # ` { A } ) = 1 )
2	1	olcd	|- ( A e. _V -> ( ( # ` { A } ) = 0 \/ ( # ` { A } ) = 1 ) )
3		snprc	|- ( -. A e. _V <-> { A } = (/) )
4	3	biimpi	|- ( -. A e. _V -> { A } = (/) )
5	4	fveq2d	|- ( -. A e. _V -> ( # ` { A } ) = ( # ` (/) ) )
6		hash0	|- ( # ` (/) ) = 0
7	5 6	eqtrdi	|- ( -. A e. _V -> ( # ` { A } ) = 0 )
8	7	orcd	|- ( -. A e. _V -> ( ( # ` { A } ) = 0 \/ ( # ` { A } ) = 1 ) )
9	2 8	pm2.61i	|- ( ( # ` { A } ) = 0 \/ ( # ` { A } ) = 1 )