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	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to F=G$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢G{Isom}_{R,S}\left(A,B\right)\to G{Isom}_{R,S}\left(A,B\right)$$
2		isocnv	$$⊢F{Isom}_{R,S}\left(A,B\right)\to F^{-1}{Isom}_{S,R}\left(B,A\right)$$
3		isotr	$$⊢\left(G{Isom}_{R,S}\left(A,B\right)\wedge F^{-1}{Isom}_{S,R}\left(B,A\right)\right)\to \left(F^{-1}\circ G\right){Isom}_{R,R}\left(A,A\right)$$
4	1 2 3	syl2anr	$$⊢\left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\to \left(F^{-1}\circ G\right){Isom}_{R,R}\left(A,A\right)$$
5		weniso	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\wedge \left(F^{-1}\circ G\right){Isom}_{R,R}\left(A,A\right)\right)\to F^{-1}\circ G={\mathrm{I}\upharpoonright }_A$$
6	5	3expa	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F^{-1}\circ G\right){Isom}_{R,R}\left(A,A\right)\right)\to F^{-1}\circ G={\mathrm{I}\upharpoonright }_A$$
7	4 6	sylan2	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to F^{-1}\circ G={\mathrm{I}\upharpoonright }_A$$
8		simprl	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to F{Isom}_{R,S}\left(A,B\right)$$
9		isof1o	$$⊢F{Isom}_{R,S}\left(A,B\right)\to F:A\underset{1-1\; onto}{⟶}B$$
10		f1of1	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A\underset{1-1}{⟶}B$$
11	8 9 10	3syl	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to F:A\underset{1-1}{⟶}B$$
12		simprr	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to G{Isom}_{R,S}\left(A,B\right)$$
13		isof1o	$$⊢G{Isom}_{R,S}\left(A,B\right)\to G:A\underset{1-1\; onto}{⟶}B$$
14		f1of1	$$⊢G:A\underset{1-1\; onto}{⟶}B\to G:A\underset{1-1}{⟶}B$$
15	12 13 14	3syl	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to G:A\underset{1-1}{⟶}B$$
16		f1eqcocnv	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge G:A\underset{1-1}{⟶}B\right)\to \left(F=G\leftrightarrow F^{-1}\circ G={\mathrm{I}\upharpoonright }_A\right)$$
17	11 15 16	syl2anc	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to \left(F=G\leftrightarrow F^{-1}\circ G={\mathrm{I}\upharpoonright }_A\right)$$
18	7 17	mpbird	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(F{Isom}_{R,S}\left(A,B\right)\wedge G{Isom}_{R,S}\left(A,B\right)\right)\right)\to F=G$$