Metamath Proof Explorer

Theorem weisoeq2

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

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

Proof

Step Hyp Ref Expression
1 isocnv 
 |-  ( F Isom R , S ( A , B ) -> `' F Isom S , R ( B , A ) )
2 isocnv 
 |-  ( G Isom R , S ( A , B ) -> `' G Isom S , R ( B , A ) )
3 1 2 anim12i 
 |-  ( ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) -> ( `' F Isom S , R ( B , A ) /\ `' G Isom S , R ( B , A ) ) )
4 weisoeq 
 |-  ( ( ( S We B /\ S Se B ) /\ ( `' F Isom S , R ( B , A ) /\ `' G Isom S , R ( B , A ) ) ) -> `' F = `' G )
5 3 4 sylan2 
 |-  ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> `' F = `' G )
6 simprl 
 |-  ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F Isom R , S ( A , B ) )
7 isof1o 
 |-  ( F Isom R , S ( A , B ) -> F : A -1-1-onto-> B )
8 f1orel 
 |-  ( F : A -1-1-onto-> B -> Rel F )
9 6 7 8 3syl 
 |-  ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> Rel F )
10 simprr 
 |-  ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> G Isom R , S ( A , B ) )
11 isof1o 
 |-  ( G Isom R , S ( A , B ) -> G : A -1-1-onto-> B )
12 f1orel 
 |-  ( G : A -1-1-onto-> B -> Rel G )
13 10 11 12 3syl 
 |-  ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> Rel G )
14 cnveqb 
 |-  ( ( Rel F /\ Rel G ) -> ( F = G <-> `' F = `' G ) )
15 9 13 14 syl2anc 
 |-  ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> ( F = G <-> `' F = `' G ) )
16 5 15 mpbird 
 |-  ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F = G )