Theorem naddword1

Description: Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	naddword1	|- ( ( A e. On /\ B e. On ) -> A C_ ( A +no B ) )

Proof

Step	Hyp	Ref	Expression
1		naddrid	|- ( A e. On -> ( A +no (/) ) = A )
2	1	adantr	|- ( ( A e. On /\ B e. On ) -> ( A +no (/) ) = A )
3		0ss	|- (/) C_ B
4		0elon	|- (/) e. On
5		naddss2	|- ( ( (/) e. On /\ B e. On /\ A e. On ) -> ( (/) C_ B <-> ( A +no (/) ) C_ ( A +no B ) ) )
6	4 5	mp3an1	|- ( ( B e. On /\ A e. On ) -> ( (/) C_ B <-> ( A +no (/) ) C_ ( A +no B ) ) )
7	6	ancoms	|- ( ( A e. On /\ B e. On ) -> ( (/) C_ B <-> ( A +no (/) ) C_ ( A +no B ) ) )
8	3 7	mpbii	|- ( ( A e. On /\ B e. On ) -> ( A +no (/) ) C_ ( A +no B ) )
9	2 8	eqsstrrd	|- ( ( A e. On /\ B e. On ) -> A C_ ( A +no B ) )