Theorem nnasmo

Description: Finite ordinal subtraction cancels on the left. (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Assertion	nnasmo	⊢ ( 𝐴 ∈ ω → ∃* 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqtr3	⊢ ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
2		nnacan	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) ↔ 𝑥 = 𝑦 ) )
3	1 2	syl5ib	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
4	3	3expb	⊢ ( ( 𝐴 ∈ ω ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
5	4	ralrimivva	⊢ ( 𝐴 ∈ ω → ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
6		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
7	6	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ( 𝐴 +o 𝑦 ) = 𝐵 ) )
8	7	rmo4	⊢ ( ∃* 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
9	5 8	sylibr	⊢ ( 𝐴 ∈ ω → ∃* 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 )