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	$⊢ S We B \to \exists^{*} f f {Isom}_{R, S} (A, B)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (S We B \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to S We B$
2		isof1o	$⊢ f {Isom}_{R, S} (A, B) \to f : A \underset{1-1 onto}{⟶} B$
3		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
4		forn	$⊢ f : A \underset{onto}{⟶} B \to ran f = B$
5	2 3 4	3syl	$⊢ f {Isom}_{R, S} (A, B) \to ran f = B$
6		vex	$⊢ f \in V$
7	6	rnex	$⊢ ran f \in V$
8	5 7	eqeltrrdi	$⊢ f {Isom}_{R, S} (A, B) \to B \in V$
9	8	ad2antrl	$⊢ (S We B \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to B \in V$
10		exse	$⊢ B \in V \to S Se B$
11	9 10	syl	$⊢ (S We B \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to S Se B$
12	1 11	jca	$⊢ (S We B \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to (S We B \land S Se B)$
13		weisoeq2	$⊢ ((S We B \land S Se B) \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to f = g$
14	12 13	sylancom	$⊢ (S We B \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to f = g$
15	14	ex	$⊢ S We B \to ((f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B)) \to f = g)$
16	15	alrimivv	$⊢ S We B \to \forall f \forall g ((f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B)) \to f = g)$
17		isoeq1	$⊢ f = g \to (f {Isom}_{R, S} (A, B) \leftrightarrow g {Isom}_{R, S} (A, B))$
18	17	mo4	$⊢ \exists^{*} f f {Isom}_{R, S} (A, B) \leftrightarrow \forall f \forall g ((f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B)) \to f = g)$
19	16 18	sylibr	$⊢ S We B \to \exists^{*} f f {Isom}_{R, S} (A, B)$