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)

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

Proof

Step	Hyp	Ref	Expression
1		1onn	|- 1o e. _om
2		php5	|- ( 1o e. _om -> -. 1o ~~ suc 1o )
3	1 2	ax-mp	|- -. 1o ~~ suc 1o
4		ensn1g	|- ( A e. _V -> { A } ~~ 1o )
5		df-2o	|- 2o = suc 1o
6	5	eqcomi	|- suc 1o = 2o
7	6	breq2i	|- ( 1o ~~ suc 1o <-> 1o ~~ 2o )
8		ensymb	|- ( { A } ~~ 1o <-> 1o ~~ { A } )
9		entr	|- ( ( 1o ~~ { A } /\ { A } ~~ 2o ) -> 1o ~~ 2o )
10	9	ex	|- ( 1o ~~ { A } -> ( { A } ~~ 2o -> 1o ~~ 2o ) )
11	8 10	sylbi	|- ( { A } ~~ 1o -> ( { A } ~~ 2o -> 1o ~~ 2o ) )
12	11	con3rr3	|- ( -. 1o ~~ 2o -> ( { A } ~~ 1o -> -. { A } ~~ 2o ) )
13	7 12	sylnbi	|- ( -. 1o ~~ suc 1o -> ( { A } ~~ 1o -> -. { A } ~~ 2o ) )
14	3 4 13	mpsyl	|- ( A e. _V -> -. { A } ~~ 2o )
15		2on0	|- 2o =/= (/)
16		ensymb	|- ( (/) ~~ 2o <-> 2o ~~ (/) )
17		en0	|- ( 2o ~~ (/) <-> 2o = (/) )
18	16 17	bitri	|- ( (/) ~~ 2o <-> 2o = (/) )
19	15 18	nemtbir	|- -. (/) ~~ 2o
20		snprc	|- ( -. A e. _V <-> { A } = (/) )
21	20	biimpi	|- ( -. A e. _V -> { A } = (/) )
22	21	breq1d	|- ( -. A e. _V -> ( { A } ~~ 2o <-> (/) ~~ 2o ) )
23	19 22	mtbiri	|- ( -. A e. _V -> -. { A } ~~ 2o )
24	14 23	pm2.61i	|- -. { A } ~~ 2o