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\left(R,A\right)$$
Assertion	oion	$$⊢A\in V\to \mathrm{dom}F\in \mathrm{On}$$

Proof

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