This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A e. On /\ B e. On ) -> ( A i^i B ) e. On )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( A e. On -> Ord A )
2 eloni 
 |-  ( B e. On -> Ord B )
3 ordin 
 |-  ( ( Ord A /\ Ord B ) -> Ord ( A i^i B ) )
4 1 2 3 syl2an 
 |-  ( ( A e. On /\ B e. On ) -> Ord ( A i^i B ) )
5 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
6 inex1g 
 |-  ( A e. On -> ( A i^i B ) e. _V )
7 elong 
 |-  ( ( A i^i B ) e. _V -> ( ( A i^i B ) e. On <-> Ord ( A i^i B ) ) )
8 5 6 7 3syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A i^i B ) e. On <-> Ord ( A i^i B ) ) )
9 4 8 mpbird 
 |-  ( ( A e. On /\ B e. On ) -> ( A i^i B ) e. On )