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 )