Metamath Proof Explorer

Theorem ordiso

Description: Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009) (Proof shortened by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	ordiso	$⊢ (A \in On \land B \in On) \to (A = B \leftrightarrow \exists f f {Isom}_{E, E} (A, B))$

Proof

Step	Hyp	Ref	Expression
1		resiexg	$⊢ A \in On \to {I ↾}_{A} \in V$
2		isoid	$⊢ ({I ↾}_{A}) {Isom}_{E, E} (A, A)$
3		isoeq1	$⊢ f = {I ↾}_{A} \to (f {Isom}_{E, E} (A, A) \leftrightarrow ({I ↾}_{A}) {Isom}_{E, E} (A, A))$
4	3	spcegv	$⊢ {I ↾}_{A} \in V \to (({I ↾}_{A}) {Isom}_{E, E} (A, A) \to \exists f f {Isom}_{E, E} (A, A))$
5	1 2 4	mpisyl	$⊢ A \in On \to \exists f f {Isom}_{E, E} (A, A)$
6	5	adantr	$⊢ (A \in On \land B \in On) \to \exists f f {Isom}_{E, E} (A, A)$
7		isoeq5	$⊢ A = B \to (f {Isom}_{E, E} (A, A) \leftrightarrow f {Isom}_{E, E} (A, B))$
8	7	exbidv	$⊢ A = B \to (\exists f f {Isom}_{E, E} (A, A) \leftrightarrow \exists f f {Isom}_{E, E} (A, B))$
9	6 8	syl5ibcom	$⊢ (A \in On \land B \in On) \to (A = B \to \exists f f {Isom}_{E, E} (A, B))$
10		eloni	$⊢ A \in On \to Ord A$
11		eloni	$⊢ B \in On \to Ord B$
12		ordiso2	$⊢ (f {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to A = B$
13	12	3coml	$⊢ (Ord A \land Ord B \land f {Isom}_{E, E} (A, B)) \to A = B$
14	13	3expia	$⊢ (Ord A \land Ord B) \to (f {Isom}_{E, E} (A, B) \to A = B)$
15	10 11 14	syl2an	$⊢ (A \in On \land B \in On) \to (f {Isom}_{E, E} (A, B) \to A = B)$
16	15	exlimdv	$⊢ (A \in On \land B \in On) \to (\exists f f {Isom}_{E, E} (A, B) \to A = B)$
17	9 16	impbid	$⊢ (A \in On \land B \in On) \to (A = B \leftrightarrow \exists f f {Isom}_{E, E} (A, B))$