Theorem oiiso

Description: The order isomorphism of the well-order R on A is an isomorphism. (Contributed by Mario Carneiro, 23-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		oicl.1	|- F = OrdIso ( R , A )
2		exse	|- ( A e. V -> R Se A )
3	1	ordtype	|- ( ( R We A /\ R Se A ) -> F Isom _E , R ( dom F , A ) )
4	3	ancoms	|- ( ( R Se A /\ R We A ) -> F Isom _E , R ( dom F , A ) )
5	2 4	sylan	|- ( ( A e. V /\ R We A ) -> F Isom _E , R ( dom F , A ) )