Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinals (continued)
sucon
Next ⟩
sucexb
Metamath Proof Explorer
Ascii
Unicode
Theorem
sucon
Description:
The class of all ordinal numbers is its own successor.
(Contributed by
NM
, 12-Sep-2003)
Ref
Expression
Assertion
sucon
⊢
suc
⁡
On
=
On
Proof
Step
Hyp
Ref
Expression
1
onprc
⊢
¬
On
∈
V
2
sucprc
⊢
¬
On
∈
V
→
suc
⁡
On
=
On
3
1
2
ax-mp
⊢
suc
⁡
On
=
On