Metamath Proof Explorer

Theorem wemoiso2

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

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

Proof

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