Theorem oninton

Description: The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of TakeutiZaring p. 44. (Contributed by NM, 29-Jan-1997)

	Ref	Expression
Assertion	oninton	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )

Proof

Step	Hyp	Ref	Expression
1		onint	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )
2	1	ex	|- ( A C_ On -> ( A =/= (/) -> |^| A e. A ) )
3		ssel	|- ( A C_ On -> ( |^| A e. A -> |^| A e. On ) )
4	2 3	syld	|- ( A C_ On -> ( A =/= (/) -> |^| A e. On ) )
5	4	imp	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )