Metamath Proof Explorer

Theorem naddss1

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

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

Proof

Step Hyp Ref Expression
1 naddel1 
 |-  ( ( B e. On /\ A e. On /\ C e. On ) -> ( B e. A <-> ( B +no C ) e. ( A +no C ) ) )
2 1 3com12 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B e. A <-> ( B +no C ) e. ( A +no C ) ) )
3 2 notbid 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. B e. A <-> -. ( B +no C ) e. ( A +no C ) ) )
4 ontri1 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) )
5 4 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> -. B e. A ) )
6 naddcl 
 |-  ( ( A e. On /\ C e. On ) -> ( A +no C ) e. On )
7 6 3adant2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no C ) e. On )
8 naddcl 
 |-  ( ( B e. On /\ C e. On ) -> ( B +no C ) e. On )
9 8 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) e. On )
10 ontri1 
 |-  ( ( ( A +no C ) e. On /\ ( B +no C ) e. On ) -> ( ( A +no C ) C_ ( B +no C ) <-> -. ( B +no C ) e. ( A +no C ) ) )
11 7 9 10 syl2anc 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no C ) C_ ( B +no C ) <-> -. ( B +no C ) e. ( A +no C ) ) )
12 3 5 11 3bitr4d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( A +no C ) C_ ( B +no C ) ) )