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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (R We A \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to R We A$
2		vex	$⊢ f \in V$
3		isof1o	$⊢ f {Isom}_{R, S} (A, B) \to f : A \underset{1-1 onto}{⟶} B$
4		f1of	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A ⟶ B$
5	3 4	syl	$⊢ f {Isom}_{R, S} (A, B) \to f : A ⟶ B$
6		dmfex	$⊢ (f \in V \land f : A ⟶ B) \to A \in V$
7	2 5 6	sylancr	$⊢ f {Isom}_{R, S} (A, B) \to A \in V$
8	7	ad2antrl	$⊢ (R We A \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to A \in V$
9		exse	$⊢ A \in V \to R Se A$
10	8 9	syl	$⊢ (R We A \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to R Se A$
11	1 10	jca	$⊢ (R We A \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to (R We A \land R Se A)$
12		weisoeq	$⊢ ((R We A \land R Se A) \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to f = g$
13	11 12	sylancom	$⊢ (R We A \land (f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B))) \to f = g$
14	13	ex	$⊢ R We A \to ((f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B)) \to f = g)$
15	14	alrimivv	$⊢ R We A \to \forall f \forall g ((f {Isom}_{R, S} (A, B) \land g {Isom}_{R, S} (A, B)) \to f = g)$
16		isoeq1	$⊢ f = g \to (f {Isom}_{R, S} (A, B) \leftrightarrow g {Isom}_{R, S} (A, B))$
17	16	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)$
18	15 17	sylibr	$⊢ R We A \to \exists^{*} f f {Isom}_{R, S} (A, B)$