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

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