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 e. V -> dom F e. On )

Proof

Step	Hyp	Ref	Expression
1		oicl.1	|- F = OrdIso ( R , A )
2	1	oicl	|- Ord dom F
3	1	oiexg	|- ( A e. V -> F e. _V )
4		dmexg	|- ( F e. _V -> dom F e. _V )
5		elong	|- ( dom F e. _V -> ( dom F e. On <-> Ord dom F ) )
6	3 4 5	3syl	|- ( A e. V -> ( dom F e. On <-> Ord dom F ) )
7	2 6	mpbiri	|- ( A e. V -> dom F e. On )