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

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2		isocnv	⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )
3		isotr	⊢ ( ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) ) → ( ◡ 𝐹 ∘ 𝐺 ) Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) )
4	1 2 3	syl2anr	⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) → ( ◡ 𝐹 ∘ 𝐺 ) Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) )
5		weniso	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ( ◡ 𝐹 ∘ 𝐺 ) Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) )
6	5	3expa	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) )
7	4 6	sylan2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) )
8		simprl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
9		isof1o	⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
10		f1of1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 )
11	8 9 10	3syl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
12		simprr	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
13		isof1o	⊢ ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐺 : 𝐴 –1-1-onto→ 𝐵 )
14		f1of1	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → 𝐺 : 𝐴 –1-1→ 𝐵 )
15	12 13 14	3syl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐺 : 𝐴 –1-1→ 𝐵 )
16		f1eqcocnv	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )
17	11 15 16	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → ( 𝐹 = 𝐺 ↔ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )
18	7 17	mpbird	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐹 = 𝐺 )