Theorem naddword1

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

	Ref	Expression
Assertion	naddword1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +no 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		naddrid	⊢ ( 𝐴 ∈ On → ( 𝐴 +no ∅ ) = 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no ∅ ) = 𝐴 )
3		0ss	⊢ ∅ ⊆ 𝐵
4		0elon	⊢ ∅ ∈ On
5		naddss2	⊢ ( ( ∅ ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐵 ↔ ( 𝐴 +no ∅ ) ⊆ ( 𝐴 +no 𝐵 ) ) )
6	4 5	mp3an1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐵 ↔ ( 𝐴 +no ∅ ) ⊆ ( 𝐴 +no 𝐵 ) ) )
7	6	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ⊆ 𝐵 ↔ ( 𝐴 +no ∅ ) ⊆ ( 𝐴 +no 𝐵 ) ) )
8	3 7	mpbii	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no ∅ ) ⊆ ( 𝐴 +no 𝐵 ) )
9	2 8	eqsstrrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +no 𝐵 ) )