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

Metamath Proof Explorer

Theorem onminesb

Description: If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of Suppes p. 228. (Contributed by NM, 29-Sep-2003)

Ref Expression
Assertion onminesb 
|- ( E. x e. On ph -> [. |^| { x e. On | ph } / x ]. ph )

Proof

Step Hyp Ref Expression
1 rabn0 
 |-  ( { x e. On | ph } =/= (/) <-> E. x e. On ph )
2 ssrab2 
 |-  { x e. On | ph } C_ On
3 onint 
 |-  ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. { x e. On | ph } )
4 2 3 mpan 
 |-  ( { x e. On | ph } =/= (/) -> |^| { x e. On | ph } e. { x e. On | ph } )
5 1 4 sylbir 
 |-  ( E. x e. On ph -> |^| { x e. On | ph } e. { x e. On | ph } )
6 nfcv 
 |-  F/_ x On
7 6 elrabsf 
 |-  ( |^| { x e. On | ph } e. { x e. On | ph } <-> ( |^| { x e. On | ph } e. On /\ [. |^| { x e. On | ph } / x ]. ph ) )
8 7 simprbi 
 |-  ( |^| { x e. On | ph } e. { x e. On | ph } -> [. |^| { x e. On | ph } / x ]. ph )
9 5 8 syl 
 |-  ( E. x e. On ph -> [. |^| { x e. On | ph } / x ]. ph )