Metamath Proof Explorer


Theorem ordin

Description: The intersection of two ordinal classes is ordinal. Proposition 7.9 of TakeutiZaring p. 37. (Contributed by NM, 9-May-1994)

Ref Expression
Assertion ordin OrdAOrdBOrdAB

Proof

Step Hyp Ref Expression
1 ordtr OrdATrA
2 ordtr OrdBTrB
3 trin TrATrBTrAB
4 1 2 3 syl2an OrdAOrdBTrAB
5 inss2 ABB
6 trssord TrABABBOrdBOrdAB
7 5 6 mp3an2 TrABOrdBOrdAB
8 4 7 sylancom OrdAOrdBOrdAB