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 ⊆ ( 𝑅1 “ On )

Proof

Step Hyp Ref Expression
1 r1fnon 𝑅1 Fn On
2 1 fndmi dom 𝑅1 = On
3 rankonidlem ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) )
4 3 simpld ( 𝑥 ∈ dom 𝑅1𝑥 ( 𝑅1 “ On ) )
5 4 ssriv dom 𝑅1 ( 𝑅1 “ On )
6 2 5 eqsstrri On ⊆ ( 𝑅1 “ On )