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 ( 𝑆 We 𝐵 → ∃* 𝑓 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝑆 We 𝐵 ∧ ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝑆 We 𝐵 )
2 isof1o ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝑓 : 𝐴1-1-onto𝐵 )
3 f1ofo ( 𝑓 : 𝐴1-1-onto𝐵𝑓 : 𝐴onto𝐵 )
4 forn ( 𝑓 : 𝐴onto𝐵 → ran 𝑓 = 𝐵 )
5 2 3 4 3syl ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ran 𝑓 = 𝐵 )
6 vex 𝑓 ∈ V
7 6 rnex ran 𝑓 ∈ V
8 5 7 eqeltrrdi ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐵 ∈ V )
9 8 ad2antrl ( ( 𝑆 We 𝐵 ∧ ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝐵 ∈ V )
10 exse ( 𝐵 ∈ V → 𝑆 Se 𝐵 )
11 9 10 syl ( ( 𝑆 We 𝐵 ∧ ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝑆 Se 𝐵 )
12 1 11 jca ( ( 𝑆 We 𝐵 ∧ ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → ( 𝑆 We 𝐵𝑆 Se 𝐵 ) )
13 weisoeq2 ( ( ( 𝑆 We 𝐵𝑆 Se 𝐵 ) ∧ ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝑓 = 𝑔 )
14 12 13 sylancom ( ( 𝑆 We 𝐵 ∧ ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) ) → 𝑓 = 𝑔 )
15 14 ex ( 𝑆 We 𝐵 → ( ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) → 𝑓 = 𝑔 ) )
16 15 alrimivv ( 𝑆 We 𝐵 → ∀ 𝑓𝑔 ( ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) → 𝑓 = 𝑔 ) )
17 isoeq1 ( 𝑓 = 𝑔 → ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) )
18 17 mo4 ( ∃* 𝑓 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ∀ 𝑓𝑔 ( ( 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑔 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) → 𝑓 = 𝑔 ) )
19 16 18 sylibr ( 𝑆 We 𝐵 → ∃* 𝑓 𝑓 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )