Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal isomorphism, Hartogs's theorem
coi
Next ⟩
df-oi
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
coi
Description:
Extend class definition to include the canonical order isomorphism to an ordinal.
Ref
Expression
Assertion
coi
class
OrdIso
R
A