This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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