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

Proof

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