Metamath Proof Explorer

Theorem nnasmo

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

Ref Expression
Assertion nnasmo 
|- ( A e. _om -> E* x e. _om ( A +o x ) = B )

Proof

Step Hyp Ref Expression
1 eqtr3 
 |-  ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> ( A +o x ) = ( A +o y ) )
2 nnacan 
 |-  ( ( A e. _om /\ x e. _om /\ y e. _om ) -> ( ( A +o x ) = ( A +o y ) <-> x = y ) )
3 1 2 syl5ib 
 |-  ( ( A e. _om /\ x e. _om /\ y e. _om ) -> ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> x = y ) )
4 3 3expb 
 |-  ( ( A e. _om /\ ( x e. _om /\ y e. _om ) ) -> ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> x = y ) )
5 4 ralrimivva 
 |-  ( A e. _om -> A. x e. _om A. y e. _om ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> x = y ) )
6 oveq2 
 |-  ( x = y -> ( A +o x ) = ( A +o y ) )
7 6 eqeq1d 
 |-  ( x = y -> ( ( A +o x ) = B <-> ( A +o y ) = B ) )
8 7 rmo4 
 |-  ( E* x e. _om ( A +o x ) = B <-> A. x e. _om A. y e. _om ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> x = y ) )
9 5 8 sylibr 
 |-  ( A e. _om -> E* x e. _om ( A +o x ) = B )