Theorem onnminsb

Description: An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. ps is the wff resulting from the substitution of A for x in wff ph . (Contributed by NM, 9-Nov-2003)

	Ref	Expression
Hypothesis	onnminsb.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	onnminsb	|- ( A e. On -> ( A e. |^| { x e. On | ph } -> -. ps ) )

Proof

Step	Hyp	Ref	Expression
1		onnminsb.1	|- ( x = A -> ( ph <-> ps ) )
2	1	elrab	|- ( A e. { x e. On | ph } <-> ( A e. On /\ ps ) )
3		ssrab2	|- { x e. On | ph } C_ On
4		onnmin	|- ( ( { x e. On | ph } C_ On /\ A e. { x e. On | ph } ) -> -. A e. |^| { x e. On | ph } )
5	3 4	mpan	|- ( A e. { x e. On | ph } -> -. A e. |^| { x e. On | ph } )
6	2 5	sylbir	|- ( ( A e. On /\ ps ) -> -. A e. |^| { x e. On | ph } )
7	6	ex	|- ( A e. On -> ( ps -> -. A e. |^| { x e. On | ph } ) )
8	7	con2d	|- ( A e. On -> ( A e. |^| { x e. On | ph } -> -. ps ) )