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