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

Metamath Proof Explorer

Theorem wemoiso

Description: Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu . (Contributed by Stefan O'Rear, 12-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion wemoiso ⊢ R We A → ∃* f f Isom R , S A B

Proof

Step Hyp Ref Expression
1 simpl ⊢ R We A ∧ f Isom R , S A B ∧ g Isom R , S A B → R We A
2 vex ⊢ f ∈ V
3 isof1o ⊢ f Isom R , S A B → f : A ⟶ 1-1 onto B
4 f1of ⊢ f : A ⟶ 1-1 onto B → f : A ⟶ B
5 3 4 syl ⊢ f Isom R , S A B → f : A ⟶ B
6 dmfex ⊢ f ∈ V ∧ f : A ⟶ B → A ∈ V
7 2 5 6 sylancr ⊢ f Isom R , S A B → A ∈ V
8 7 ad2antrl ⊢ R We A ∧ f Isom R , S A B ∧ g Isom R , S A B → A ∈ V
9 exse ⊢ A ∈ V → R Se A
10 8 9 syl ⊢ R We A ∧ f Isom R , S A B ∧ g Isom R , S A B → R Se A
11 1 10 jca ⊢ R We A ∧ f Isom R , S A B ∧ g Isom R , S A B → R We A ∧ R Se A
12 weisoeq ⊢ R We A ∧ R Se A ∧ f Isom R , S A B ∧ g Isom R , S A B → f = g
13 11 12 sylancom ⊢ R We A ∧ f Isom R , S A B ∧ g Isom R , S A B → f = g
14 13 ex ⊢ R We A → f Isom R , S A B ∧ g Isom R , S A B → f = g
15 14 alrimivv ⊢ R We A → ∀ f ∀ g f Isom R , S A B ∧ g Isom R , S A B → f = g
16 isoeq1 ⊢ f = g → f Isom R , S A B ↔ g Isom R , S A B
17 16 mo4 ⊢ ∃* f f Isom R , S A B ↔ ∀ f ∀ g f Isom R , S A B ∧ g Isom R , S A B → f = g
18 15 17 sylibr ⊢ R We A → ∃* f f Isom R , S A B