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	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω )
2		eqid	⊢ ( ℕ ∩ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) ) = ( ℕ ∩ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) )
3		eqid	⊢ ( ω ∩ ( ◡ ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) = ( ω ∩ ( ◡ ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
4		eqid	⊢ OrdIso ( 𝑅 , 𝐴 ) = OrdIso ( 𝑅 , 𝐴 )
5	1 2 3 4	fz1isolem	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )