Metamath Proof Explorer

Theorem naddel12

Description: Natural addition to both sides of ordinal less-than. (Contributed by Scott Fenton, 7-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> B e. D )
2 onelon 
 |-  ( ( D e. On /\ B e. D ) -> B e. On )
3 2 ad2ant2l 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> B e. On )
4 simplr 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> D e. On )
5 onelon 
 |-  ( ( C e. On /\ A e. C ) -> A e. On )
6 5 ad2ant2r 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> A e. On )
7 naddel2 
 |-  ( ( B e. On /\ D e. On /\ A e. On ) -> ( B e. D <-> ( A +no B ) e. ( A +no D ) ) )
8 3 4 6 7 syl3anc 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( B e. D <-> ( A +no B ) e. ( A +no D ) ) )
9 1 8 mpbid 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no B ) e. ( A +no D ) )
10 simprl 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> A e. C )
11 simpll 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> C e. On )
12 naddel1 
 |-  ( ( A e. On /\ C e. On /\ D e. On ) -> ( A e. C <-> ( A +no D ) e. ( C +no D ) ) )
13 6 11 4 12 syl3anc 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A e. C <-> ( A +no D ) e. ( C +no D ) ) )
14 10 13 mpbid 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no D ) e. ( C +no D ) )
15 naddcl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +no D ) e. On )
16 15 adantr 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( C +no D ) e. On )
17 ontr1 
 |-  ( ( C +no D ) e. On -> ( ( ( A +no B ) e. ( A +no D ) /\ ( A +no D ) e. ( C +no D ) ) -> ( A +no B ) e. ( C +no D ) ) )
18 16 17 syl 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( ( ( A +no B ) e. ( A +no D ) /\ ( A +no D ) e. ( C +no D ) ) -> ( A +no B ) e. ( C +no D ) ) )
19 9 14 18 mp2and 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no B ) e. ( C +no D ) )
20 19 ex 
 |-  ( ( C e. On /\ D e. On ) -> ( ( A e. C /\ B e. D ) -> ( A +no B ) e. ( C +no D ) ) )