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	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		isocnv	⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )
2		isocnv	⊢ ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐺 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )
3	1 2	anim12i	⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) → ( ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) ∧ ◡ 𝐺 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) ) )
4		weisoeq	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) ∧ ◡ 𝐺 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) ) ) → ◡ 𝐹 = ◡ 𝐺 )
5	3 4	sylan2	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → ◡ 𝐹 = ◡ 𝐺 )
6		simprl	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
7		isof1o	⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
8		f1orel	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐹 )
9	6 7 8	3syl	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → Rel 𝐹 )
10		simprr	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
11		isof1o	⊢ ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐺 : 𝐴 –1-1-onto→ 𝐵 )
12		f1orel	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐺 )
13	10 11 12	3syl	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → Rel 𝐺 )
14		cnveqb	⊢ ( ( Rel 𝐹 ∧ Rel 𝐺 ) → ( 𝐹 = 𝐺 ↔ ◡ 𝐹 = ◡ 𝐺 ) )
15	9 13 14	syl2anc	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → ( 𝐹 = 𝐺 ↔ ◡ 𝐹 = ◡ 𝐺 ) )
16	5 15	mpbird	⊢ ( ( ( 𝑆 We 𝐵 ∧ 𝑆 Se 𝐵 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐹 = 𝐺 )