This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 → ( 𝒫 𝐴 ∩ 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 bitrid ⊢ ( Ord 𝐴 → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ On ) ↔ 𝑥 ∈ suc 𝐴 ) )
17 16 eqrdv ⊢ ( Ord 𝐴 → ( 𝒫 𝐴 ∩ On ) = suc 𝐴 )