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 ) )