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

Metamath Proof Explorer

Theorem onminsb

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

Ref Expression
Hypotheses onminsb.1 
|- F/ x ps
onminsb.2 
|- ( x = |^| { x e. On | ph } -> ( ph <-> ps ) )
Assertion onminsb 
|- ( E. x e. On ph -> ps )

Proof

Step Hyp Ref Expression
1 onminsb.1 
 |-  F/ x ps
2 onminsb.2 
 |-  ( x = |^| { x e. On | ph } -> ( ph <-> ps ) )
3 rabn0 
 |-  ( { x e. On | ph } =/= (/) <-> E. x e. On ph )
4 ssrab2 
 |-  { x e. On | ph } C_ On
5 onint 
 |-  ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. { x e. On | ph } )
6 4 5 mpan 
 |-  ( { x e. On | ph } =/= (/) -> |^| { x e. On | ph } e. { x e. On | ph } )
7 3 6 sylbir 
 |-  ( E. x e. On ph -> |^| { x e. On | ph } e. { x e. On | ph } )
8 nfrab1 
 |-  F/_ x { x e. On | ph }
9 8 nfint 
 |-  F/_ x |^| { x e. On | ph }
10 nfcv 
 |-  F/_ x On
11 9 10 1 2 elrabf 
 |-  ( |^| { x e. On | ph } e. { x e. On | ph } <-> ( |^| { x e. On | ph } e. On /\ ps ) )
12 11 simprbi 
 |-  ( |^| { x e. On | ph } e. { x e. On | ph } -> ps )
13 7 12 syl 
 |-  ( E. x e. On ph -> ps )