Metamath Proof Explorer

Theorem onwf

Description: The ordinals are all well-founded. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion onwf 
|- On C_ U. ( R1 " On )

Proof

Step Hyp Ref Expression
1 r1fnon 
 |-  R1 Fn On
2 1 fndmi 
 |-  dom R1 = On
3 rankonidlem 
 |-  ( x e. dom R1 -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) )
4 3 simpld 
 |-  ( x e. dom R1 -> x e. U. ( R1 " On ) )
5 4 ssriv 
 |-  dom R1 C_ U. ( R1 " On )
6 2 5 eqsstrri 
 |-  On C_ U. ( R1 " On )