Theorem naddword2

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

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

Proof

Step	Hyp	Ref	Expression
1		naddword1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +no 𝐵 ) )
2		naddcom	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ( 𝐵 +no 𝐴 ) )
3	1 2	sseqtrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐵 +no 𝐴 ) )