Metamath Proof Explorer

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 On A A On


Step Hyp Ref Expression
1 onint A On A A A
2 1 ex A On A A A
3 ssel A On A A A On
4 2 3 syld A On A A On
5 4 imp A On A A On