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 ⊢ R Or A ∧ A ∈ Fin → ∃ f f Isom < , R 1 … A A

Proof

Step Hyp Ref Expression
1 eqid ⊢ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω
2 eqid ⊢ ℕ ∩ < -1 A + 1 = ℕ ∩ < -1 A + 1
3 eqid ⊢ ω ∩ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω -1 ⁡ A + 1 = ω ∩ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω -1 ⁡ A + 1
4 eqid ⊢ OrdIso R A = OrdIso R A
5 1 2 3 4 fz1isolem ⊢ R Or A ∧ A ∈ Fin → ∃ f f Isom < , R 1 … A A