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

Proof

Step	Hyp	Ref	Expression
1		oicl.1	$$⊢F=OrdIso\left(R,A\right)$$
2	1	oiexg	$$⊢A\in V\to F\in \mathrm{V}$$
3	1	oiiso	$$⊢\left(A\in V\wedge R\mathrm{We}A\right)\to F{Isom}_{\mathrm{E},R}\left(\mathrm{dom}F,A\right)$$
4		isof1o	$$⊢F{Isom}_{\mathrm{E},R}\left(\mathrm{dom}F,A\right)\to F:\mathrm{dom}F\underset{1-1\; onto}{⟶}A$$
5	3 4	syl	$$⊢\left(A\in V\wedge R\mathrm{We}A\right)\to F:\mathrm{dom}F\underset{1-1\; onto}{⟶}A$$
6		f1oen3g	$$⊢\left(F\in \mathrm{V}\wedge F:\mathrm{dom}F\underset{1-1\; onto}{⟶}A\right)\to \mathrm{dom}F\approx A$$
7	2 5 6	syl2an2r	$$⊢\left(A\in V\wedge R\mathrm{We}A\right)\to \mathrm{dom}F\approx A$$