Metamath Proof Explorer

Theorem oemapwe

Description: The lexicographic order on a function space of ordinals gives a well-ordering with order type equal to the ordinal exponential. This provides an alternate definition of the ordinal exponential. (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
oemapval.t 
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
Assertion oemapwe 
|- ( ph -> ( T We S /\ dom OrdIso ( T , S ) = ( A ^o B ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 oemapval.t 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
6 2 3 5 syl2anc 
 |-  ( ph -> ( A ^o B ) e. On )
7 eloni 
 |-  ( ( A ^o B ) e. On -> Ord ( A ^o B ) )
8 ordwe 
 |-  ( Ord ( A ^o B ) -> _E We ( A ^o B ) )
9 6 7 8 3syl 
 |-  ( ph -> _E We ( A ^o B ) )
10 1 2 3 4 cantnf 
 |-  ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) )
11 isowe 
 |-  ( ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) -> ( T We S <-> _E We ( A ^o B ) ) )
12 10 11 syl 
 |-  ( ph -> ( T We S <-> _E We ( A ^o B ) ) )
13 9 12 mpbird 
 |-  ( ph -> T We S )
14 6 7 syl 
 |-  ( ph -> Ord ( A ^o B ) )
15 isocnv 
 |-  ( ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) -> `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) )
16 10 15 syl 
 |-  ( ph -> `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) )
17 ovex 
 |-  ( A CNF B ) e. _V
18 17 dmex 
 |-  dom ( A CNF B ) e. _V
19 1 18 eqeltri 
 |-  S e. _V
20 exse 
 |-  ( S e. _V -> T Se S )
21 19 20 ax-mp 
 |-  T Se S
22 eqid 
 |-  OrdIso ( T , S ) = OrdIso ( T , S )
23 22 oieu 
 |-  ( ( T We S /\ T Se S ) -> ( ( Ord ( A ^o B ) /\ `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) <-> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) ) )
24 13 21 23 sylancl 
 |-  ( ph -> ( ( Ord ( A ^o B ) /\ `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) <-> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) ) )
25 14 16 24 mpbi2and 
 |-  ( ph -> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) )
26 25 simpld 
 |-  ( ph -> ( A ^o B ) = dom OrdIso ( T , S ) )
27 26 eqcomd 
 |-  ( ph -> dom OrdIso ( T , S ) = ( A ^o B ) )
28 13 27 jca 
 |-  ( ph -> ( T We S /\ dom OrdIso ( T , S ) = ( A ^o B ) ) )