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 * 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 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 V f : A B A V
7 2 5 6 sylancr f Isom R , S A B A V
8 7 ad2antrl R We A f Isom R , S A B g Isom R , S A B A V
9 exse A 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 f 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 * f f Isom R , S A B f g f Isom R , S A B g Isom R , S A B f = g
18 15 17 sylibr R We A * f f Isom R , S A B