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

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 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )