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 ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ A + C ∈ B + C

Proof

Step Hyp Ref Expression
1 naddelim ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A + C ∈ B + C
2 naddssim ⊢ B ∈ On ∧ A ∈ On ∧ C ∈ On → B ⊆ A → B + C ⊆ A + C
3 2 3com12 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ⊆ A → B + C ⊆ A + C
4 ontri1 ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ ¬ A ∈ B
5 4 ancoms ⊢ A ∈ On ∧ B ∈ On → B ⊆ A ↔ ¬ A ∈ B
6 5 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ⊆ A ↔ ¬ A ∈ B
7 naddcl ⊢ B ∈ On ∧ C ∈ On → B + C ∈ On
8 7 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C ∈ On
9 naddcl ⊢ A ∈ On ∧ C ∈ On → A + C ∈ On
10 ontri1 ⊢ B + C ∈ On ∧ A + C ∈ On → B + C ⊆ A + C ↔ ¬ A + C ∈ B + C
11 8 9 10 3imp3i2an ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C ⊆ A + C ↔ ¬ A + C ∈ B + C
12 3 6 11 3imtr3d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ A ∈ B → ¬ A + C ∈ B + C
13 1 12 impcon4bid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ A + C ∈ B + C