In recent years, artificial intelligence has greatly contributed to the development of formal theorem proving, and formal verification of basic mathematical theories can improve the credibility of proofs and increase their automation. The ordinal number, as an important mathematical object for the concept of infinity, is widely used in different areas of research because of its well-ordered character. This work systematically establishes the ordinal number within the Morse-Kelley (MK) axiomatic set theory framework using the Coq proof assistant. We rigorously derive and validate fundamental ordinal properties through MK-based definitions, like transitivity, antisymmetry, trichotomy, and non-density. Building on the classification of the ordinal number (void, successor, and non-void limit), we formalize the second form of transfinite induction and verify that the ordinal number is an extension of the nonnegative integer. The work addresses the oversimplified proofs in the traditional literature and lays a formal foundation for advanced studies of ordinal arithmetic and fundamental theorems.