Metamath Proof Explorer

Theorem omsucelsucb

Description: Membership is inherited by successors for natural numbers. (Contributed by AV, 15-Sep-2023)

Ref Expression
Assertion omsucelsucb ⊢ N ∈ ω ↔ suc ⁡ N ∈ suc ⁡ ω

Proof

Step Hyp Ref Expression
1 ordom ⊢ Ord ⁡ ω
2 ordsucelsuc ⊢ Ord ⁡ ω → N ∈ ω ↔ suc ⁡ N ∈ suc ⁡ ω
3 1 2 ax-mp ⊢ N ∈ ω ↔ suc ⁡ N ∈ suc ⁡ ω