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

Metamath Proof Explorer

Theorem onminex

Description: If a wff is true for an ordinal number, then there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997) (Proof shortened by Mario Carneiro, 20-Nov-2016)

Ref Expression
Hypothesis onminex.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion onminex 
|- ( E. x e. On ph -> E. x e. On ( ph /\ A. y e. x -. ps ) )

Proof

Step Hyp Ref Expression
1 onminex.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 ssrab2 
 |-  { x e. On | ph } C_ On
3 rabn0 
 |-  ( { x e. On | ph } =/= (/) <-> E. x e. On ph )
4 3 biimpri 
 |-  ( E. x e. On ph -> { x e. On | ph } =/= (/) )
5 oninton 
 |-  ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. On )
6 2 4 5 sylancr 
 |-  ( E. x e. On ph -> |^| { x e. On | ph } e. On )
7 onminesb 
 |-  ( E. x e. On ph -> [. |^| { x e. On | ph } / x ]. ph )
8 onss 
 |-  ( |^| { x e. On | ph } e. On -> |^| { x e. On | ph } C_ On )
9 6 8 syl 
 |-  ( E. x e. On ph -> |^| { x e. On | ph } C_ On )
10 9 sseld 
 |-  ( E. x e. On ph -> ( y e. |^| { x e. On | ph } -> y e. On ) )
11 1 onnminsb 
 |-  ( y e. On -> ( y e. |^| { x e. On | ph } -> -. ps ) )
12 10 11 syli 
 |-  ( E. x e. On ph -> ( y e. |^| { x e. On | ph } -> -. ps ) )
13 12 ralrimiv 
 |-  ( E. x e. On ph -> A. y e. |^| { x e. On | ph } -. ps )
14 dfsbcq2 
 |-  ( z = |^| { x e. On | ph } -> ( [ z / x ] ph <-> [. |^| { x e. On | ph } / x ]. ph ) )
15 raleq 
 |-  ( z = |^| { x e. On | ph } -> ( A. y e. z -. ps <-> A. y e. |^| { x e. On | ph } -. ps ) )
16 14 15 anbi12d 
 |-  ( z = |^| { x e. On | ph } -> ( ( [ z / x ] ph /\ A. y e. z -. ps ) <-> ( [. |^| { x e. On | ph } / x ]. ph /\ A. y e. |^| { x e. On | ph } -. ps ) ) )
17 16 rspcev 
 |-  ( ( |^| { x e. On | ph } e. On /\ ( [. |^| { x e. On | ph } / x ]. ph /\ A. y e. |^| { x e. On | ph } -. ps ) ) -> E. z e. On ( [ z / x ] ph /\ A. y e. z -. ps ) )
18 6 7 13 17 syl12anc 
 |-  ( E. x e. On ph -> E. z e. On ( [ z / x ] ph /\ A. y e. z -. ps ) )
19 nfv 
 |-  F/ z ( ph /\ A. y e. x -. ps )
20 nfs1v 
 |-  F/ x [ z / x ] ph
21 nfv 
 |-  F/ x A. y e. z -. ps
22 20 21 nfan 
 |-  F/ x ( [ z / x ] ph /\ A. y e. z -. ps )
23 sbequ12 
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
24 raleq 
 |-  ( x = z -> ( A. y e. x -. ps <-> A. y e. z -. ps ) )
25 23 24 anbi12d 
 |-  ( x = z -> ( ( ph /\ A. y e. x -. ps ) <-> ( [ z / x ] ph /\ A. y e. z -. ps ) ) )
26 19 22 25 cbvrexw 
 |-  ( E. x e. On ( ph /\ A. y e. x -. ps ) <-> E. z e. On ( [ z / x ] ph /\ A. y e. z -. ps ) )
27 18 26 sylibr 
 |-  ( E. x e. On ph -> E. x e. On ( ph /\ A. y e. x -. ps ) )