This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 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 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )