Metamath Proof Explorer


Theorem onin

Description: The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995)

Ref Expression
Assertion onin AOnBOnABOn

Proof

Step Hyp Ref Expression
1 eloni AOnOrdA
2 eloni BOnOrdB
3 ordin OrdAOrdBOrdAB
4 1 2 3 syl2an AOnBOnOrdAB
5 simpl AOnBOnAOn
6 inex1g AOnABV
7 elong ABVABOnOrdAB
8 5 6 7 3syl AOnBOnABOnOrdAB
9 4 8 mpbird AOnBOnABOn