Metamath Proof Explorer


Theorem naddss2

Description: Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024)

Ref Expression
Assertion naddss2
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( C +no A ) C_ ( C +no B ) ) )

Proof

Step Hyp Ref Expression
1 naddss1
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( A +no C ) C_ ( B +no C ) ) )
2 naddcom
 |-  ( ( A e. On /\ C e. On ) -> ( A +no C ) = ( C +no A ) )
3 2 3adant2
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no C ) = ( C +no A ) )
4 naddcom
 |-  ( ( B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) )
5 4 3adant1
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) )
6 3 5 sseq12d
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no C ) C_ ( B +no C ) <-> ( C +no A ) C_ ( C +no B ) ) )
7 1 6 bitrd
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( C +no A ) C_ ( C +no B ) ) )