Theorem sn1dom

Description: A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023)

	Ref	Expression
Assertion	sn1dom	|- { A } ~<_ 1o

Proof

Step	Hyp	Ref	Expression
1		ensn1g	|- ( A e. _V -> { A } ~~ 1o )
2		1on	|- 1o e. On
3		domrefg	|- ( 1o e. On -> 1o ~<_ 1o )
4	2 3	ax-mp	|- 1o ~<_ 1o
5		endomtr	|- ( ( { A } ~~ 1o /\ 1o ~<_ 1o ) -> { A } ~<_ 1o )
6	1 4 5	sylancl	|- ( A e. _V -> { A } ~<_ 1o )
7		snprc	|- ( -. A e. _V <-> { A } = (/) )
8		snex	|- { A } e. _V
9		eqeng	|- ( { A } e. _V -> ( { A } = (/) -> { A } ~~ (/) ) )
10	8 9	ax-mp	|- ( { A } = (/) -> { A } ~~ (/) )
11	7 10	sylbi	|- ( -. A e. _V -> { A } ~~ (/) )
12		0domg	|- ( 1o e. On -> (/) ~<_ 1o )
13	2 12	ax-mp	|- (/) ~<_ 1o
14		endomtr	|- ( ( { A } ~~ (/) /\ (/) ~<_ 1o ) -> { A } ~<_ 1o )
15	11 13 14	sylancl	|- ( -. A e. _V -> { A } ~<_ 1o )
16	6 15	pm2.61i	|- { A } ~<_ 1o