Theorem onminsb 6631

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

Hypotheses

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

Assertion

Ref	Expression
onminsb	|- ( E. x e. On ph -> ps )

Proof of Theorem onminsb

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

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1446   F/wnf 1669   e. wcel 1889   =/= wne 2624   E.wrex 2740   {crab 2743   C_ wss 3406   (/)c0 3733   |^|cint 4237   Oncon0 5426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-br 4406  df-opab 4465  df-tr 4501  df-eprel 4748  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-ord 5429  df-on 5430

This theorem is referenced by:  oawordeulem  7260  rankidb  8276  cardmin2  8437  cardaleph  8525  cardmin  8994