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 -1 Isom S , R B A
3 isotr ⊢ G Isom R , S A B ∧ F -1 Isom S , R B A → F -1 ∘ G Isom R , R A A
4 1 2 3 syl2anr ⊢ F Isom R , S A B ∧ G Isom R , S A B → F -1 ∘ G Isom R , R A A
5 weniso ⊢ R We A ∧ R Se A ∧ F -1 ∘ G Isom R , R A A → F -1 ∘ G = I ↾ A
6 5 3expa ⊢ R We A ∧ R Se A ∧ F -1 ∘ G Isom R , R A A → F -1 ∘ 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 -1 ∘ 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 -1 ∘ 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 -1 ∘ 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