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

Metamath Proof Explorer

Theorem onunisuc

Description: An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994) Generalize from onunisuci . (Revised by BJ, 28-Dec-2024)

Ref Expression
Assertion onunisuc ⊢ A ∈ On → ⋃ suc ⁡ A = A

Proof

Step Hyp Ref Expression
1 ontr ⊢ A ∈ On → Tr ⁡ A
2 unisucg ⊢ A ∈ On → Tr ⁡ A ↔ ⋃ suc ⁡ A = A
3 1 2 mpbid ⊢ A ∈ On → ⋃ suc ⁡ A = A