Theorem oien

Description: The order type of a well-ordered set is equinumerous to the set. (Contributed by Mario Carneiro, 23-May-2015)

	Ref	Expression
Hypothesis	oicl.1	|- F = OrdIso ( R , A )
Assertion	oien	|- ( ( A e. V /\ R We A ) -> dom F ~~ A )

Proof

Step	Hyp	Ref	Expression
1		oicl.1	|- F = OrdIso ( R , A )
2	1	oiexg	|- ( A e. V -> F e. _V )
3	1	oiiso	|- ( ( A e. V /\ R We A ) -> F Isom _E , R ( dom F , A ) )
4		isof1o	|- ( F Isom _E , R ( dom F , A ) -> F : dom F -1-1-onto-> A )
5	3 4	syl	|- ( ( A e. V /\ R We A ) -> F : dom F -1-1-onto-> A )
6		f1oen3g	|- ( ( F e. _V /\ F : dom F -1-1-onto-> A ) -> dom F ~~ A )
7	2 5 6	syl2an2r	|- ( ( A e. V /\ R We A ) -> dom F ~~ A )