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

Metamath Proof Explorer

Theorem onenon

Description: Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	onenon	$⊢ A \in On \to A \in dom card$

Step	Hyp	Ref	Expression
1		enrefg	$⊢ A \in On \to A \approx A$
2		isnumi	$⊢ (A \in On \land A \approx A) \to A \in dom card$
3	1 2	mpdan	$⊢ A \in On \to A \in dom card$