Metamath Proof Explorer


Theorem onssmin

Description: A nonempty class of ordinal numbers has the smallest member. Exercise 9 of TakeutiZaring p. 40. (Contributed by NM, 3-Oct-2003)

Ref Expression
Assertion onssmin AOnAxAyAxy

Proof

Step Hyp Ref Expression
1 onint AOnAAA
2 intss1 yAAy
3 2 rgen yAAy
4 sseq1 x=AxyAy
5 4 ralbidv x=AyAxyyAAy
6 5 rspcev AAyAAyxAyAxy
7 1 3 6 sylancl AOnAxAyAxy