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