Theorem 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 𝐴 → ( 𝒫 𝐴 ∩ On ) = suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ On ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ∈ On ) )
2		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
3	2	anbi2ci	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ∈ On ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝐴 ) )
4	1 3	bitri	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ On ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝐴 ) )
5		ordsssuc	⊢ ( ( 𝑥 ∈ On ∧ Ord 𝐴 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ∈ suc 𝐴 ) )
6	5	expcom	⊢ ( Ord 𝐴 → ( 𝑥 ∈ On → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ∈ suc 𝐴 ) ) )
7	6	pm5.32d	⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ suc 𝐴 ) ) )
8		simpr	⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ suc 𝐴 ) → 𝑥 ∈ suc 𝐴 )
9		ordsuc	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
10		ordelon	⊢ ( ( Ord suc 𝐴 ∧ 𝑥 ∈ suc 𝐴 ) → 𝑥 ∈ On )
11	10	ex	⊢ ( Ord suc 𝐴 → ( 𝑥 ∈ suc 𝐴 → 𝑥 ∈ On ) )
12	9 11	sylbi	⊢ ( Ord 𝐴 → ( 𝑥 ∈ suc 𝐴 → 𝑥 ∈ On ) )
13	12	ancrd	⊢ ( Ord 𝐴 → ( 𝑥 ∈ suc 𝐴 → ( 𝑥 ∈ On ∧ 𝑥 ∈ suc 𝐴 ) ) )
14	8 13	impbid2	⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑥 ∈ suc 𝐴 ) ↔ 𝑥 ∈ suc 𝐴 ) )
15	7 14	bitrd	⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝐴 ) ↔ 𝑥 ∈ suc 𝐴 ) )
16	4 15	syl5bb	⊢ ( Ord 𝐴 → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ On ) ↔ 𝑥 ∈ suc 𝐴 ) )
17	16	eqrdv	⊢ ( Ord 𝐴 → ( 𝒫 𝐴 ∩ On ) = suc 𝐴 )