Metamath Proof Explorer

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 ⁡ A → 𝒫 A ∩ On = suc ⁡ A

Proof

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