Metamath Proof Explorer

Theorem oion

Description: The order type of the well-order R on A is an ordinal. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 23-May-2015)

		Ref	Expression
	Hypothesis	oicl.1	$⊢ F = OrdIso (R, A)$
	Assertion	oion	$⊢ A \in V \to dom F \in On$

Proof

Step	Hyp	Ref	Expression
1		oicl.1	$⊢ F = OrdIso (R, A)$
2	1	oicl	$⊢ Ord dom F$
3	1	oiexg	$⊢ A \in V \to F \in V$
4		dmexg	$⊢ F \in V \to dom F \in V$
5		elong	$⊢ dom F \in V \to (dom F \in On \leftrightarrow Ord dom F)$
6	3 4 5	3syl	$⊢ A \in V \to (dom F \in On \leftrightarrow Ord dom F)$
7	2 6	mpbiri	$⊢ A \in V \to dom F \in On$