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

Metamath Proof Explorer

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 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐹 = 𝐺 )