ordpwsuc

Description: The collection of ordinals in the power class of an ordinal is its successor. (Contributed by NM, 30-Jan-2005)

		Ref	Expression
	Assertion	ordpwsuc	$⊢ Ord A \to 𝒫 A \cap On = suc A$

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (𝒫 A \cap On) \leftrightarrow (x \in 𝒫 A \land x \in On)$
2		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
3	2	anbi2ci	$⊢ (x \in 𝒫 A \land x \in On) \leftrightarrow (x \in On \land x \subseteq A)$
4	1 3	bitri	$⊢ x \in (𝒫 A \cap On) \leftrightarrow (x \in On \land x \subseteq A)$
5		ordsssuc	$⊢ (x \in On \land Ord A) \to (x \subseteq A \leftrightarrow x \in suc A)$
6	5	expcom	$⊢ Ord A \to (x \in On \to (x \subseteq A \leftrightarrow x \in suc A))$
7	6	pm5.32d	$⊢ Ord A \to ((x \in On \land x \subseteq A) \leftrightarrow (x \in On \land x \in suc A))$
8		simpr	$⊢ (x \in On \land x \in suc A) \to x \in suc A$
9		ordsuc	$⊢ Ord A \leftrightarrow Ord suc A$
10		ordelon	$⊢ (Ord suc A \land x \in suc A) \to x \in On$
11	10	ex	$⊢ Ord suc A \to (x \in suc A \to x \in On)$
12	9 11	sylbi	$⊢ Ord A \to (x \in suc A \to x \in On)$
13	12	ancrd	$⊢ Ord A \to (x \in suc A \to (x \in On \land x \in suc A))$
14	8 13	impbid2	$⊢ Ord A \to ((x \in On \land x \in suc A) \leftrightarrow x \in suc A)$
15	7 14	bitrd	$⊢ Ord A \to ((x \in On \land x \subseteq A) \leftrightarrow x \in suc A)$
16	4 15	bitrid	$⊢ Ord A \to (x \in (𝒫 A \cap On) \leftrightarrow x \in suc A)$
17	16	eqrdv	$⊢ Ord A \to 𝒫 A \cap On = suc A$

Metamath Proof Explorer