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 Ord A Ord B Ord A B


Step Hyp Ref Expression
1 ordtr Ord A Tr A
2 ordtr Ord B Tr B
3 trin Tr A Tr B Tr A B
4 1 2 3 syl2an Ord A Ord B Tr A B
5 inss2 A B B
6 trssord Tr A B A B B Ord B Ord A B
7 5 6 mp3an2 Tr A B Ord B Ord A B
8 4 7 sylancom Ord A Ord B Ord A B