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 e. On /\ B e. On ) -> ( A = B <-> E. f f Isom _E , _E ( A , B ) ) )

Proof

Step	Hyp	Ref	Expression
1		resiexg	|- ( A e. On -> ( _I |` A ) e. _V )
2		isoid	|- ( _I |` A ) Isom _E , _E ( A , A )
3		isoeq1	|- ( f = ( _I |` A ) -> ( f Isom _E , _E ( A , A ) <-> ( _I |` A ) Isom _E , _E ( A , A ) ) )
4	3	spcegv	|- ( ( _I |` A ) e. _V -> ( ( _I |` A ) Isom _E , _E ( A , A ) -> E. f f Isom _E , _E ( A , A ) ) )
5	1 2 4	mpisyl	|- ( A e. On -> E. f f Isom _E , _E ( A , A ) )
6	5	adantr	|- ( ( A e. On /\ B e. On ) -> E. f f Isom _E , _E ( A , A ) )
7		isoeq5	|- ( A = B -> ( f Isom _E , _E ( A , A ) <-> f Isom _E , _E ( A , B ) ) )
8	7	exbidv	|- ( A = B -> ( E. f f Isom _E , _E ( A , A ) <-> E. f f Isom _E , _E ( A , B ) ) )
9	6 8	syl5ibcom	|- ( ( A e. On /\ B e. On ) -> ( A = B -> E. f f Isom _E , _E ( A , B ) ) )
10		eloni	|- ( A e. On -> Ord A )
11		eloni	|- ( B e. On -> Ord B )
12		ordiso2	|- ( ( f Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A = B )
13	12	3coml	|- ( ( Ord A /\ Ord B /\ f Isom _E , _E ( A , B ) ) -> A = B )
14	13	3expia	|- ( ( Ord A /\ Ord B ) -> ( f Isom _E , _E ( A , B ) -> A = B ) )
15	10 11 14	syl2an	|- ( ( A e. On /\ B e. On ) -> ( f Isom _E , _E ( A , B ) -> A = B ) )
16	15	exlimdv	|- ( ( A e. On /\ B e. On ) -> ( E. f f Isom _E , _E ( A , B ) -> A = B ) )
17	9 16	impbid	|- ( ( A e. On /\ B e. On ) -> ( A = B <-> E. f f Isom _E , _E ( A , B ) ) )