# 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 ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \exists !{f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}OrdIso\left({R},{A}\right)=OrdIso\left({R},{A}\right)$
2 1 oiexg ${⊢}{A}\in \mathrm{Fin}\to OrdIso\left({R},{A}\right)\in \mathrm{V}$
3 2 adantl ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to OrdIso\left({R},{A}\right)\in \mathrm{V}$
4 simpr ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to {A}\in \mathrm{Fin}$
5 wofi ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to {R}\mathrm{We}{A}$
6 1 oiiso ${⊢}\left({A}\in \mathrm{Fin}\wedge {R}\mathrm{We}{A}\right)\to OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{dom}OrdIso\left({R},{A}\right),{A}\right)$
7 4 5 6 syl2anc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{dom}OrdIso\left({R},{A}\right),{A}\right)$
8 1 oien ${⊢}\left({A}\in \mathrm{Fin}\wedge {R}\mathrm{We}{A}\right)\to \mathrm{dom}OrdIso\left({R},{A}\right)\approx {A}$
9 4 5 8 syl2anc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \mathrm{dom}OrdIso\left({R},{A}\right)\approx {A}$
10 ficardid ${⊢}{A}\in \mathrm{Fin}\to \mathrm{card}\left({A}\right)\approx {A}$
11 10 adantl ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \mathrm{card}\left({A}\right)\approx {A}$
12 11 ensymd ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to {A}\approx \mathrm{card}\left({A}\right)$
13 entr ${⊢}\left(\mathrm{dom}OrdIso\left({R},{A}\right)\approx {A}\wedge {A}\approx \mathrm{card}\left({A}\right)\right)\to \mathrm{dom}OrdIso\left({R},{A}\right)\approx \mathrm{card}\left({A}\right)$
14 9 12 13 syl2anc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \mathrm{dom}OrdIso\left({R},{A}\right)\approx \mathrm{card}\left({A}\right)$
15 1 oion ${⊢}{A}\in \mathrm{Fin}\to \mathrm{dom}OrdIso\left({R},{A}\right)\in \mathrm{On}$
16 15 adantl ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \mathrm{dom}OrdIso\left({R},{A}\right)\in \mathrm{On}$
17 ficardom ${⊢}{A}\in \mathrm{Fin}\to \mathrm{card}\left({A}\right)\in \mathrm{\omega }$
18 17 adantl ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \mathrm{card}\left({A}\right)\in \mathrm{\omega }$
19 onomeneq ${⊢}\left(\mathrm{dom}OrdIso\left({R},{A}\right)\in \mathrm{On}\wedge \mathrm{card}\left({A}\right)\in \mathrm{\omega }\right)\to \left(\mathrm{dom}OrdIso\left({R},{A}\right)\approx \mathrm{card}\left({A}\right)↔\mathrm{dom}OrdIso\left({R},{A}\right)=\mathrm{card}\left({A}\right)\right)$
20 16 18 19 syl2anc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \left(\mathrm{dom}OrdIso\left({R},{A}\right)\approx \mathrm{card}\left({A}\right)↔\mathrm{dom}OrdIso\left({R},{A}\right)=\mathrm{card}\left({A}\right)\right)$
21 14 20 mpbid ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \mathrm{dom}OrdIso\left({R},{A}\right)=\mathrm{card}\left({A}\right)$
22 isoeq4 ${⊢}\mathrm{dom}OrdIso\left({R},{A}\right)=\mathrm{card}\left({A}\right)\to \left(OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{dom}OrdIso\left({R},{A}\right),{A}\right)↔OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)\right)$
23 21 22 syl ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \left(OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{dom}OrdIso\left({R},{A}\right),{A}\right)↔OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)\right)$
24 7 23 mpbid ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)$
25 isoeq1 ${⊢}{f}=OrdIso\left({R},{A}\right)\to \left({f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)↔OrdIso\left({R},{A}\right){Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)\right)$
26 3 24 25 spcedv ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)$
27 wemoiso2 ${⊢}{R}\mathrm{We}{A}\to {\exists }^{*}{f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)$
28 5 27 syl ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to {\exists }^{*}{f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)$
29 df-eu ${⊢}\exists !{f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)↔\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)\wedge {\exists }^{*}{f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)\right)$
30 26 28 29 sylanbrc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \exists !{f}\phantom{\rule{.4em}{0ex}}{f}{Isom}_{\mathrm{E},{R}}\left(\mathrm{card}\left({A}\right),{A}\right)$