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 On D On A C B D A + B C + D

Proof

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