Metamath Proof Explorer

Theorem isnum2

Description: A way to express well-orderability without bound or distinct variables. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion isnum2 
|- ( A e. dom card <-> E. x e. On x ~~ A )

Proof

Step Hyp Ref Expression
1 cardf2 
 |-  card : { y | E. x e. On x ~~ y } --> On
2 1 fdmi 
 |-  dom card = { y | E. x e. On x ~~ y }
3 2 eleq2i 
 |-  ( A e. dom card <-> A e. { y | E. x e. On x ~~ y } )
4 relen 
 |-  Rel ~~
5 4 brrelex2i 
 |-  ( x ~~ A -> A e. _V )
6 5 rexlimivw 
 |-  ( E. x e. On x ~~ A -> A e. _V )
7 breq2 
 |-  ( y = A -> ( x ~~ y <-> x ~~ A ) )
8 7 rexbidv 
 |-  ( y = A -> ( E. x e. On x ~~ y <-> E. x e. On x ~~ A ) )
9 6 8 elab3 
 |-  ( A e. { y | E. x e. On x ~~ y } <-> E. x e. On x ~~ A )
10 3 9 bitri 
 |-  ( A e. dom card <-> E. x e. On x ~~ A )