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 \subseteq ⋃ R_{1} [On]$

Step	Hyp	Ref	Expression
1		r1fnon	$⊢ R_{1} Fn On$
2	1	fndmi	$⊢ dom R_{1} = On$
3		rankonidlem	$⊢ x \in dom R_{1} \to (x \in ⋃ R_{1} [On] \land rank (x) = x)$
4	3	simpld	$⊢ x \in dom R_{1} \to x \in ⋃ R_{1} [On]$
5	4	ssriv	$⊢ dom R_{1} \subseteq ⋃ R_{1} [On]$
6	2 5	eqsstrri	$⊢ On \subseteq ⋃ R_{1} [On]$