Metamath Proof Explorer


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 ) )