Theorem fz1iso

Description: Any finite ordered set has an order isomorphism to a one-based finite sequence. (Contributed by Mario Carneiro, 2-Apr-2014)

	Ref	Expression
Assertion	fz1iso	$$⊢\left(R\mathrm{Or}A\wedge A\in \mathrm{Fin}\right)\to \exists ff{Isom}_{<,R}\left(\left(1\dots \left|A\right|\right),A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n+1\right),1\right)\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n+1\right),1\right)\upharpoonright }_{\mathrm{\omega }}$$
2		eqid	$$⊢\mathbb{N}\cap {<}^{-1}\left[\left\{\left|A\right|+1\right\}\right]=\mathbb{N}\cap {<}^{-1}\left[\left\{\left|A\right|+1\right\}\right]$$
3		eqid	$$⊢\mathrm{\omega }\cap {\left({\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n+1\right),1\right)\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(\left|A\right|+1\right)=\mathrm{\omega }\cap {\left({\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n+1\right),1\right)\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(\left|A\right|+1\right)$$
4		eqid	$$⊢OrdIso\left(R,A\right)=OrdIso\left(R,A\right)$$
5	1 2 3 4	fz1isolem	$$⊢\left(R\mathrm{Or}A\wedge A\in \mathrm{Fin}\right)\to \exists ff{Isom}_{<,R}\left(\left(1\dots \left|A\right|\right),A\right)$$