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	|- ( ( A C_ On /\ A =/= (/) ) -> E. x e. A A. y e. A x C_ y )

Proof

Step	Hyp	Ref	Expression
1		onint	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )
2		intss1	|- ( y e. A -> |^| A C_ y )
3	2	rgen	|- A. y e. A |^| A C_ y
4		sseq1	|- ( x = |^| A -> ( x C_ y <-> |^| A C_ y ) )
5	4	ralbidv	|- ( x = |^| A -> ( A. y e. A x C_ y <-> A. y e. A |^| A C_ y ) )
6	5	rspcev	|- ( ( |^| A e. A /\ A. y e. A |^| A C_ y ) -> E. x e. A A. y e. A x C_ y )
7	1 3 6	sylancl	|- ( ( A C_ On /\ A =/= (/) ) -> E. x e. A A. y e. A x C_ y )