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		fndm	⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
3	1 2	ax-mp	⊢ dom 𝑅1 = On
4		rankonidlem	⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) )
5	4	simpld	⊢ ( 𝑥 ∈ dom 𝑅1 → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
6	5	ssriv	⊢ dom 𝑅1 ⊆ ∪ ( 𝑅1 “ On )
7	3 6	eqsstrri	⊢ On ⊆ ∪ ( 𝑅1 “ On )