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 e. Fin ) -> E! 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 e. Fin -> OrdIso ( R , A ) e. _V )
3 2 adantl 
 |-  ( ( R Or A /\ A e. Fin ) -> OrdIso ( R , A ) e. _V )
4 simpr 
 |-  ( ( R Or A /\ A e. Fin ) -> A e. Fin )
5 wofi 
 |-  ( ( R Or A /\ A e. Fin ) -> R We A )
6 1 oiiso 
 |-  ( ( A e. Fin /\ R We A ) -> OrdIso ( R , A ) Isom _E , R ( dom OrdIso ( R , A ) , A ) )
7 4 5 6 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> OrdIso ( R , A ) Isom _E , R ( dom OrdIso ( R , A ) , A ) )
8 1 oien 
 |-  ( ( A e. Fin /\ R We A ) -> dom OrdIso ( R , A ) ~~ A )
9 4 5 8 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> dom OrdIso ( R , A ) ~~ A )
10 ficardid 
 |-  ( A e. Fin -> ( card ` A ) ~~ A )
11 10 adantl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( card ` A ) ~~ A )
12 11 ensymd 
 |-  ( ( R Or A /\ A e. 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 e. Fin ) -> dom OrdIso ( R , A ) ~~ ( card ` A ) )
15 1 oion 
 |-  ( A e. Fin -> dom OrdIso ( R , A ) e. On )
16 15 adantl 
 |-  ( ( R Or A /\ A e. Fin ) -> dom OrdIso ( R , A ) e. On )
17 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
18 17 adantl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( card ` A ) e. _om )
19 onomeneq 
 |-  ( ( dom OrdIso ( R , A ) e. On /\ ( card ` A ) e. _om ) -> ( dom OrdIso ( R , A ) ~~ ( card ` A ) <-> dom OrdIso ( R , A ) = ( card ` A ) ) )
20 16 18 19 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> ( dom OrdIso ( R , A ) ~~ ( card ` A ) <-> dom OrdIso ( R , A ) = ( card ` A ) ) )
21 14 20 mpbid 
 |-  ( ( R Or A /\ A e. 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 e. 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 e. 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 e. Fin ) -> E. f f Isom _E , R ( ( card ` A ) , A ) )
27 wemoiso2 
 |-  ( R We A -> E* f f Isom _E , R ( ( card ` A ) , A ) )
28 5 27 syl 
 |-  ( ( R Or A /\ A e. Fin ) -> E* f f Isom _E , R ( ( card ` A ) , A ) )
29 df-eu 
 |-  ( E! f f Isom _E , R ( ( card ` A ) , A ) <-> ( E. f f Isom _E , R ( ( card ` A ) , A ) /\ E* f f Isom _E , R ( ( card ` A ) , A ) ) )
30 26 28 29 sylanbrc 
 |-  ( ( R Or A /\ A e. Fin ) -> E! f f Isom _E , R ( ( card ` A ) , A ) )