This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnasmo

Description: There is at most one left additive inverse for natural number addition. (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 imbitrid ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( 𝐴 +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 𝑥 ) = 𝐵 )