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\left(R,A\right)$$
Assertion	oiiso	$$⊢\left(A\in V\wedge R\mathrm{We}A\right)\to F{Isom}_{\mathrm{E},R}\left(\mathrm{dom}F,A\right)$$

Proof

Step	Hyp	Ref	Expression
1		oicl.1	$$⊢F=OrdIso\left(R,A\right)$$
2		exse	$$⊢A\in V\to R\mathrm{Se}A$$
3	1	ordtype	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to F{Isom}_{\mathrm{E},R}\left(\mathrm{dom}F,A\right)$$
4	3	ancoms	$$⊢\left(R\mathrm{Se}A\wedge R\mathrm{We}A\right)\to F{Isom}_{\mathrm{E},R}\left(\mathrm{dom}F,A\right)$$
5	2 4	sylan	$$⊢\left(A\in V\wedge R\mathrm{We}A\right)\to F{Isom}_{\mathrm{E},R}\left(\mathrm{dom}F,A\right)$$