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