# 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 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \mathrm{Ord}\left({A}\cap {B}\right)$

### Proof

Step Hyp Ref Expression
1 ordtr ${⊢}\mathrm{Ord}{A}\to \mathrm{Tr}{A}$
2 ordtr ${⊢}\mathrm{Ord}{B}\to \mathrm{Tr}{B}$
3 trin ${⊢}\left(\mathrm{Tr}{A}\wedge \mathrm{Tr}{B}\right)\to \mathrm{Tr}\left({A}\cap {B}\right)$
4 1 2 3 syl2an ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \mathrm{Tr}\left({A}\cap {B}\right)$
5 inss2 ${⊢}{A}\cap {B}\subseteq {B}$
6 trssord ${⊢}\left(\mathrm{Tr}\left({A}\cap {B}\right)\wedge {A}\cap {B}\subseteq {B}\wedge \mathrm{Ord}{B}\right)\to \mathrm{Ord}\left({A}\cap {B}\right)$
7 5 6 mp3an2 ${⊢}\left(\mathrm{Tr}\left({A}\cap {B}\right)\wedge \mathrm{Ord}{B}\right)\to \mathrm{Ord}\left({A}\cap {B}\right)$
8 4 7 sylancom ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \mathrm{Ord}\left({A}\cap {B}\right)$