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 \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to F = G$

Proof

Step	Hyp	Ref	Expression
1		isocnv	$⊢ F {Isom}_{R, S} (A, B) \to F^{-1} {Isom}_{S, R} (B, A)$
2		isocnv	$⊢ G {Isom}_{R, S} (A, B) \to G^{-1} {Isom}_{S, R} (B, A)$
3	1 2	anim12i	$⊢ (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B)) \to (F^{-1} {Isom}_{S, R} (B, A) \land G^{-1} {Isom}_{S, R} (B, A))$
4		weisoeq	$⊢ ((S We B \land S Se B) \land (F^{-1} {Isom}_{S, R} (B, A) \land G^{-1} {Isom}_{S, R} (B, A))) \to F^{-1} = G^{-1}$
5	3 4	sylan2	$⊢ ((S We B \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to F^{-1} = G^{-1}$
6		simprl	$⊢ ((S We B \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to F {Isom}_{R, S} (A, B)$
7		isof1o	$⊢ F {Isom}_{R, S} (A, B) \to F : A \underset{1-1 onto}{⟶} B$
8		f1orel	$⊢ F : A \underset{1-1 onto}{⟶} B \to Rel F$
9	6 7 8	3syl	$⊢ ((S We B \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to Rel F$
10		simprr	$⊢ ((S We B \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to G {Isom}_{R, S} (A, B)$
11		isof1o	$⊢ G {Isom}_{R, S} (A, B) \to G : A \underset{1-1 onto}{⟶} B$
12		f1orel	$⊢ G : A \underset{1-1 onto}{⟶} B \to Rel G$
13	10 11 12	3syl	$⊢ ((S We B \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to Rel G$
14		cnveqb	$⊢ (Rel F \land Rel G) \to (F = G \leftrightarrow F^{-1} = G^{-1})$
15	9 13 14	syl2anc	$⊢ ((S We B \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to (F = G \leftrightarrow F^{-1} = G^{-1})$
16	5 15	mpbird	$⊢ ((S We B \land S Se B) \land (F {Isom}_{R, S} (A, B) \land G {Isom}_{R, S} (A, B))) \to F = G$