Metamath Proof Explorer

Theorem numthcor

Description: Any set is strictly dominated by some ordinal. (Contributed by NM, 22-Oct-2003)

Ref Expression
Assertion numthcor 
|- ( A e. V -> E. x e. On A ~< x )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = A -> ( y ~< x <-> A ~< x ) )
2 1 rexbidv 
 |-  ( y = A -> ( E. x e. On y ~< x <-> E. x e. On A ~< x ) )
3 vpwex 
 |-  ~P y e. _V
4 3 numth2 
 |-  E. x e. On x ~~ ~P y
5 vex 
 |-  y e. _V
6 5 canth2 
 |-  y ~< ~P y
7 ensym 
 |-  ( x ~~ ~P y -> ~P y ~~ x )
8 sdomentr 
 |-  ( ( y ~< ~P y /\ ~P y ~~ x ) -> y ~< x )
9 6 7 8 sylancr 
 |-  ( x ~~ ~P y -> y ~< x )
10 9 reximi 
 |-  ( E. x e. On x ~~ ~P y -> E. x e. On y ~< x )
11 4 10 ax-mp 
 |-  E. x e. On y ~< x
12 2 11 vtoclg 
 |-  ( A e. V -> E. x e. On A ~< x )