This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) )