Theorem hashen1

Description: A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019)

	Ref	Expression
Assertion	hashen1	|- ( A e. V -> ( ( # ` A ) = 1 <-> A ~~ 1o ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		hashsng	|- ( (/) e. _V -> ( # ` { (/) } ) = 1 )
3	1 2	ax-mp	|- ( # ` { (/) } ) = 1
4	3	eqcomi	|- 1 = ( # ` { (/) } )
5	4	a1i	|- ( A e. V -> 1 = ( # ` { (/) } ) )
6	5	eqeq2d	|- ( A e. V -> ( ( # ` A ) = 1 <-> ( # ` A ) = ( # ` { (/) } ) ) )
7		simpr	|- ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> ( # ` A ) = ( # ` { (/) } ) )
8		1nn0	|- 1 e. NN0
9	3 8	eqeltri	|- ( # ` { (/) } ) e. NN0
10		hashvnfin	|- ( ( A e. V /\ ( # ` { (/) } ) e. NN0 ) -> ( ( # ` A ) = ( # ` { (/) } ) -> A e. Fin ) )
11	9 10	mpan2	|- ( A e. V -> ( ( # ` A ) = ( # ` { (/) } ) -> A e. Fin ) )
12	11	imp	|- ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> A e. Fin )
13		snfi	|- { (/) } e. Fin
14		hashen	|- ( ( A e. Fin /\ { (/) } e. Fin ) -> ( ( # ` A ) = ( # ` { (/) } ) <-> A ~~ { (/) } ) )
15	12 13 14	sylancl	|- ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> ( ( # ` A ) = ( # ` { (/) } ) <-> A ~~ { (/) } ) )
16	7 15	mpbid	|- ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> A ~~ { (/) } )
17	16	ex	|- ( A e. V -> ( ( # ` A ) = ( # ` { (/) } ) -> A ~~ { (/) } ) )
18		hasheni	|- ( A ~~ { (/) } -> ( # ` A ) = ( # ` { (/) } ) )
19	17 18	impbid1	|- ( A e. V -> ( ( # ` A ) = ( # ` { (/) } ) <-> A ~~ { (/) } ) )
20		df1o2	|- 1o = { (/) }
21	20	eqcomi	|- { (/) } = 1o
22	21	breq2i	|- ( A ~~ { (/) } <-> A ~~ 1o )
23	22	a1i	|- ( A e. V -> ( A ~~ { (/) } <-> A ~~ 1o ) )
24	6 19 23	3bitrd	|- ( A e. V -> ( ( # ` A ) = 1 <-> A ~~ 1o ) )