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