Metamath Proof Explorer


Theorem wemoiso

Description: Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu . (Contributed by Stefan O'Rear, 12-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion wemoiso
|- ( R We A -> E* f f Isom R , S ( A , B ) )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> R We A )
2 vex
 |-  f e. _V
3 isof1o
 |-  ( f Isom R , S ( A , B ) -> f : A -1-1-onto-> B )
4 f1of
 |-  ( f : A -1-1-onto-> B -> f : A --> B )
5 3 4 syl
 |-  ( f Isom R , S ( A , B ) -> f : A --> B )
6 dmfex
 |-  ( ( f e. _V /\ f : A --> B ) -> A e. _V )
7 2 5 6 sylancr
 |-  ( f Isom R , S ( A , B ) -> A e. _V )
8 7 ad2antrl
 |-  ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> A e. _V )
9 exse
 |-  ( A e. _V -> R Se A )
10 8 9 syl
 |-  ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> R Se A )
11 1 10 jca
 |-  ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> ( R We A /\ R Se A ) )
12 weisoeq
 |-  ( ( ( R We A /\ R Se A ) /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> f = g )
13 11 12 sylancom
 |-  ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> f = g )
14 13 ex
 |-  ( R We A -> ( ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) -> f = g ) )
15 14 alrimivv
 |-  ( R We A -> A. f A. g ( ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) -> f = g ) )
16 isoeq1
 |-  ( f = g -> ( f Isom R , S ( A , B ) <-> g Isom R , S ( A , B ) ) )
17 16 mo4
 |-  ( E* f f Isom R , S ( A , B ) <-> A. f A. g ( ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) -> f = g ) )
18 15 17 sylibr
 |-  ( R We A -> E* f f Isom R , S ( A , B ) )