Metamath Proof Explorer

Theorem weisoeq

Description: Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso . (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion weisoeq 
|- ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F = G )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( G Isom R , S ( A , B ) -> G Isom R , S ( A , B ) )
2 isocnv 
 |-  ( F Isom R , S ( A , B ) -> `' F Isom S , R ( B , A ) )
3 isotr 
 |-  ( ( G Isom R , S ( A , B ) /\ `' F Isom S , R ( B , A ) ) -> ( `' F o. G ) Isom R , R ( A , A ) )
4 1 2 3 syl2anr 
 |-  ( ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) -> ( `' F o. G ) Isom R , R ( A , A ) )
5 weniso 
 |-  ( ( R We A /\ R Se A /\ ( `' F o. G ) Isom R , R ( A , A ) ) -> ( `' F o. G ) = ( _I |` A ) )
6 5 3expa 
 |-  ( ( ( R We A /\ R Se A ) /\ ( `' F o. G ) Isom R , R ( A , A ) ) -> ( `' F o. G ) = ( _I |` A ) )
7 4 6 sylan2 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> ( `' F o. G ) = ( _I |` A ) )
8 simprl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F Isom R , S ( A , B ) )
9 isof1o 
 |-  ( F Isom R , S ( A , B ) -> F : A -1-1-onto-> B )
10 f1of1 
 |-  ( F : A -1-1-onto-> B -> F : A -1-1-> B )
11 8 9 10 3syl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F : A -1-1-> B )
12 simprr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> G Isom R , S ( A , B ) )
13 isof1o 
 |-  ( G Isom R , S ( A , B ) -> G : A -1-1-onto-> B )
14 f1of1 
 |-  ( G : A -1-1-onto-> B -> G : A -1-1-> B )
15 12 13 14 3syl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> G : A -1-1-> B )
16 f1eqcocnv 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( F = G <-> ( `' F o. G ) = ( _I |` A ) ) )
17 11 15 16 syl2anc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> ( F = G <-> ( `' F o. G ) = ( _I |` A ) ) )
18 7 17 mpbird 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F = G )