Theorem snnen2o

Description: A singleton { A } is never equinumerous with the ordinal number 2. This holds for proper singletons ( A e.V ) as well as for singletons being the empty set ( A e/ V ). (Contributed by AV, 6-Aug-2019) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	snnen2o	|- -. { A } ~~ 2o

Proof

Step	Hyp	Ref	Expression
1		df2o3	|- 2o = { (/) , 1o }
2		0ex	|- (/) e. _V
3		1oex	|- 1o e. _V
4		1n0	|- 1o =/= (/)
5	4	necomi	|- (/) =/= 1o
6		prnesn	|- ( ( (/) e. _V /\ 1o e. _V /\ (/) =/= 1o ) -> { (/) , 1o } =/= { x } )
7	2 3 5 6	mp3an	|- { (/) , 1o } =/= { x }
8	1 7	eqnetri	|- 2o =/= { x }
9	8	neii	|- -. 2o = { x }
10	9	nex	|- -. E. x 2o = { x }
11		2on0	|- 2o =/= (/)
12		f1cdmsn	|- ( ( `' f : 2o -1-1-> { A } /\ 2o =/= (/) ) -> E. x 2o = { x } )
13	11 12	mpan2	|- ( `' f : 2o -1-1-> { A } -> E. x 2o = { x } )
14	10 13	mto	|- -. `' f : 2o -1-1-> { A }
15		f1ocnv	|- ( f : { A } -1-1-onto-> 2o -> `' f : 2o -1-1-onto-> { A } )
16		f1of1	|- ( `' f : 2o -1-1-onto-> { A } -> `' f : 2o -1-1-> { A } )
17	15 16	syl	|- ( f : { A } -1-1-onto-> 2o -> `' f : 2o -1-1-> { A } )
18	14 17	mto	|- -. f : { A } -1-1-onto-> 2o
19	18	nex	|- -. E. f f : { A } -1-1-onto-> 2o
20		snex	|- { A } e. _V
21		2oex	|- 2o e. _V
22		breng	|- ( ( { A } e. _V /\ 2o e. _V ) -> ( { A } ~~ 2o <-> E. f f : { A } -1-1-onto-> 2o ) )
23	20 21 22	mp2an	|- ( { A } ~~ 2o <-> E. f f : { A } -1-1-onto-> 2o )
24	19 23	mtbir	|- -. { A } ~~ 2o