Metamath Proof Explorer

Theorem wemoiso2

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

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

Proof

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