Metamath Proof Explorer

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 
|- ( ( R Or A /\ A e. Fin ) -> E. f f Isom < , R ( ( 1 ... ( # ` A ) ) , A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) = ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om )
2 eqid 
 |-  ( NN i^i ( `' < " { ( ( # ` A ) + 1 ) } ) ) = ( NN i^i ( `' < " { ( ( # ` A ) + 1 ) } ) )
3 eqid 
 |-  ( _om i^i ( `' ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` ( ( # ` A ) + 1 ) ) ) = ( _om i^i ( `' ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` ( ( # ` A ) + 1 ) ) )
4 eqid 
 |-  OrdIso ( R , A ) = OrdIso ( R , A )
5 1 2 3 4 fz1isolem 
 |-  ( ( R Or A /\ A e. Fin ) -> E. f f Isom < , R ( ( 1 ... ( # ` A ) ) , A ) )