Theorem omsucelsucb

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

	Ref	Expression
Assertion	omsucelsucb	$$⊢N\in \mathrm{\omega }\leftrightarrow \mathrm{suc}N\in \mathrm{suc}\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
2		ordsucelsuc	$$⊢\mathrm{Ord}\mathrm{\omega }\to \left(N\in \mathrm{\omega }\leftrightarrow \mathrm{suc}N\in \mathrm{suc}\mathrm{\omega }\right)$$
3	1 2	ax-mp	$$⊢N\in \mathrm{\omega }\leftrightarrow \mathrm{suc}N\in \mathrm{suc}\mathrm{\omega }$$