This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 -1 Isom S , R B A
2 isocnv ⊢ G Isom R , S A B → G -1 Isom S , R B A
3 1 2 anim12i ⊢ F Isom R , S A B ∧ G Isom R , S A B → F -1 Isom S , R B A ∧ G -1 Isom S , R B A
4 weisoeq ⊢ S We B ∧ S Se B ∧ F -1 Isom S , R B A ∧ G -1 Isom S , R B A → F -1 = G -1
5 3 4 sylan2 ⊢ S We B ∧ S Se B ∧ F Isom R , S A B ∧ G Isom R , S A B → F -1 = G -1
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 -1 = G -1
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 -1 = G -1
16 5 15 mpbird ⊢ S We B ∧ S Se B ∧ F Isom R , S A B ∧ G Isom R , S A B → F = G