Metamath Proof Explorer

Theorem naddel1

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

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

Proof

Step Hyp Ref Expression
1 naddelim 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B -> ( A +no C ) e. ( B +no C ) ) )
2 naddssim 
 |-  ( ( B e. On /\ A e. On /\ C e. On ) -> ( B C_ A -> ( B +no C ) C_ ( A +no C ) ) )
3 2 3com12 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B C_ A -> ( B +no C ) C_ ( A +no C ) ) )
4 ontri1 
 |-  ( ( B e. On /\ A e. On ) -> ( B C_ A <-> -. A e. B ) )
5 4 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( B C_ A <-> -. A e. B ) )
6 5 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B C_ A <-> -. A e. B ) )
7 naddcl 
 |-  ( ( B e. On /\ C e. On ) -> ( B +no C ) e. On )
8 7 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) e. On )
9 naddcl 
 |-  ( ( A e. On /\ C e. On ) -> ( A +no C ) e. On )
10 ontri1 
 |-  ( ( ( B +no C ) e. On /\ ( A +no C ) e. On ) -> ( ( B +no C ) C_ ( A +no C ) <-> -. ( A +no C ) e. ( B +no C ) ) )
11 8 9 10 3imp3i2an 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( B +no C ) C_ ( A +no C ) <-> -. ( A +no C ) e. ( B +no C ) ) )
12 3 6 11 3imtr3d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. A e. B -> -. ( A +no C ) e. ( B +no C ) ) )
13 1 12 impcon4bid 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( A +no C ) e. ( B +no C ) ) )