Metamath Proof Explorer

Theorem naddelim

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

Ref Expression
Assertion naddelim ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A + C ∈ B + C

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ b = A → b + C = A + C
2 1 eleq1d ⊢ b = A → b + C ∈ x ↔ A + C ∈ x
3 2 rspcv ⊢ A ∈ B → ∀ b ∈ B b + C ∈ x → A + C ∈ x
4 3 ad2antlr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ∈ B ∧ x ∈ On → ∀ b ∈ B b + C ∈ x → A + C ∈ x
5 4 adantld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ∈ B ∧ x ∈ On → ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x → A + C ∈ x
6 5 ralrimiva ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ∈ B → ∀ x ∈ On ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x → A + C ∈ x
7 ovex ⊢ A + C ∈ V
8 7 elintrab ⊢ A + C ∈ ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x ↔ ∀ x ∈ On ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x → A + C ∈ x
9 6 8 sylibr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ∈ B → A + C ∈ ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x
10 naddov2 ⊢ B ∈ On ∧ C ∈ On → B + C = ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x
11 10 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C = ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x
12 11 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ∈ B → B + C = ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x
13 9 12 eleqtrrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ∈ B → A + C ∈ B + C
14 13 ex ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A + C ∈ B + C