This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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