Metamath Proof Explorer

Theorem finnisoeu

Description: A finite totally ordered set has a unique order isomorphism to a finite ordinal. (Contributed by Stefan O'Rear, 16-Nov-2014) (Proof shortened by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion finnisoeu ⊢ R Or A ∧ A ∈ Fin → ∃! f f Isom E , R card ⁡ A A

Proof

Step Hyp Ref Expression
1 eqid ⊢ OrdIso R A = OrdIso R A
2 1 oiexg ⊢ A ∈ Fin → OrdIso R A ∈ V
3 2 adantl ⊢ R Or A ∧ A ∈ Fin → OrdIso R A ∈ V
4 simpr ⊢ R Or A ∧ A ∈ Fin → A ∈ Fin
5 wofi ⊢ R Or A ∧ A ∈ Fin → R We A
6 1 oiiso ⊢ A ∈ Fin ∧ R We A → OrdIso R A Isom E , R dom ⁡ OrdIso R A A
7 4 5 6 syl2anc ⊢ R Or A ∧ A ∈ Fin → OrdIso R A Isom E , R dom ⁡ OrdIso R A A
8 1 oien ⊢ A ∈ Fin ∧ R We A → dom ⁡ OrdIso R A ≈ A
9 4 5 8 syl2anc ⊢ R Or A ∧ A ∈ Fin → dom ⁡ OrdIso R A ≈ A
10 ficardid ⊢ A ∈ Fin → card ⁡ A ≈ A
11 10 adantl ⊢ R Or A ∧ A ∈ Fin → card ⁡ A ≈ A
12 11 ensymd ⊢ R Or A ∧ A ∈ Fin → A ≈ card ⁡ A
13 entr ⊢ dom ⁡ OrdIso R A ≈ A ∧ A ≈ card ⁡ A → dom ⁡ OrdIso R A ≈ card ⁡ A
14 9 12 13 syl2anc ⊢ R Or A ∧ A ∈ Fin → dom ⁡ OrdIso R A ≈ card ⁡ A
15 1 oion ⊢ A ∈ Fin → dom ⁡ OrdIso R A ∈ On
16 15 adantl ⊢ R Or A ∧ A ∈ Fin → dom ⁡ OrdIso R A ∈ On
17 ficardom ⊢ A ∈ Fin → card ⁡ A ∈ ω
18 17 adantl ⊢ R Or A ∧ A ∈ Fin → card ⁡ A ∈ ω
19 onomeneq ⊢ dom ⁡ OrdIso R A ∈ On ∧ card ⁡ A ∈ ω → dom ⁡ OrdIso R A ≈ card ⁡ A ↔ dom ⁡ OrdIso R A = card ⁡ A
20 16 18 19 syl2anc ⊢ R Or A ∧ A ∈ Fin → dom ⁡ OrdIso R A ≈ card ⁡ A ↔ dom ⁡ OrdIso R A = card ⁡ A
21 14 20 mpbid ⊢ R Or A ∧ A ∈ Fin → dom ⁡ OrdIso R A = card ⁡ A
22 isoeq4 ⊢ dom ⁡ OrdIso R A = card ⁡ A → OrdIso R A Isom E , R dom ⁡ OrdIso R A A ↔ OrdIso R A Isom E , R card ⁡ A A
23 21 22 syl ⊢ R Or A ∧ A ∈ Fin → OrdIso R A Isom E , R dom ⁡ OrdIso R A A ↔ OrdIso R A Isom E , R card ⁡ A A
24 7 23 mpbid ⊢ R Or A ∧ A ∈ Fin → OrdIso R A Isom E , R card ⁡ A A
25 isoeq1 ⊢ f = OrdIso R A → f Isom E , R card ⁡ A A ↔ OrdIso R A Isom E , R card ⁡ A A
26 3 24 25 spcedv ⊢ R Or A ∧ A ∈ Fin → ∃ f f Isom E , R card ⁡ A A
27 wemoiso2 ⊢ R We A → ∃* f f Isom E , R card ⁡ A A
28 5 27 syl ⊢ R Or A ∧ A ∈ Fin → ∃* f f Isom E , R card ⁡ A A
29 df-eu ⊢ ∃! f f Isom E , R card ⁡ A A ↔ ∃ f f Isom E , R card ⁡ A A ∧ ∃* f f Isom E , R card ⁡ A A
30 26 28 29 sylanbrc ⊢ R Or A ∧ A ∈ Fin → ∃! f f Isom E , R card ⁡ A A