Theorem onpwsuc

Description: The collection of ordinal numbers in the power set of an ordinal number is its successor. (Contributed by NM, 19-Oct-2004)

	Ref	Expression
Assertion	onpwsuc	$$⊢A\in \mathrm{On}\to 𝒫A\cap \mathrm{On}=\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		ordpwsuc	$$⊢\mathrm{Ord}A\to 𝒫A\cap \mathrm{On}=\mathrm{suc}A$$
3	1 2	syl	$$⊢A\in \mathrm{On}\to 𝒫A\cap \mathrm{On}=\mathrm{suc}A$$