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 )