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 i^i B ) )

Proof

Step Hyp Ref Expression
1 ordtr 
 |-  ( Ord A -> Tr A )
2 ordtr 
 |-  ( Ord B -> Tr B )
3 trin 
 |-  ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )
4 1 2 3 syl2an 
 |-  ( ( Ord A /\ Ord B ) -> Tr ( A i^i B ) )
5 inss2 
 |-  ( A i^i B ) C_ B
6 trssord 
 |-  ( ( Tr ( A i^i B ) /\ ( A i^i B ) C_ B /\ Ord B ) -> Ord ( A i^i B ) )
7 5 6 mp3an2 
 |-  ( ( Tr ( A i^i B ) /\ Ord B ) -> Ord ( A i^i B ) )
8 4 7 sylancom 
 |-  ( ( Ord A /\ Ord B ) -> Ord ( A i^i B ) )