MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-oi Unicode version

Definition df-oi 7179
Description: Define the canonical order isomorphism from the well-order  R on  A to an ordinal. (Contributed by Mario Carneiro, 23-May-2015.)
Assertion
Ref Expression
df-oi  |- OrdIso ( R ,  A )  =  if ( ( R  We  A  /\  R Se  A ) ,  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )  |`  { x  e.  On  |  E. t  e.  A  A. z  e.  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t } ) ,  (/) )
Distinct variable groups:    h, j,
t, u, v, w, x, z, A    R, h, j, t, u, v, w, x, z

Detailed syntax breakdown of Definition df-oi
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2coi 7178 . 2  class OrdIso ( R ,  A )
41, 2wwe 4309 . . . 4  wff  R  We  A
51, 2wse 4308 . . . 4  wff  R Se  A
64, 5wa 360 . . 3  wff  ( R  We  A  /\  R Se  A )
7 vh . . . . . 6  set  h
8 cvv 2757 . . . . . 6  class  _V
9 vu . . . . . . . . . . 11  set  u
109cv 1618 . . . . . . . . . 10  class  u
11 vv . . . . . . . . . . 11  set  v
1211cv 1618 . . . . . . . . . 10  class  v
1310, 12, 2wbr 3983 . . . . . . . . 9  wff  u R v
1413wn 5 . . . . . . . 8  wff  -.  u R v
15 vj . . . . . . . . . . . 12  set  j
1615cv 1618 . . . . . . . . . . 11  class  j
17 vw . . . . . . . . . . . 12  set  w
1817cv 1618 . . . . . . . . . . 11  class  w
1916, 18, 2wbr 3983 . . . . . . . . . 10  wff  j R w
207cv 1618 . . . . . . . . . . 11  class  h
2120crn 4648 . . . . . . . . . 10  class  ran  h
2219, 15, 21wral 2516 . . . . . . . . 9  wff  A. j  e.  ran  h  j R w
2322, 17, 1crab 2520 . . . . . . . 8  class  { w  e.  A  |  A. j  e.  ran  h  j R w }
2414, 9, 23wral 2516 . . . . . . 7  wff  A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v
2524, 11, 23crio 6249 . . . . . 6  class  ( iota_ v  e.  { w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v )
267, 8, 25cmpt 4037 . . . . 5  class  ( h  e.  _V  |->  ( iota_ v  e.  { w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) )
2726crecs 6341 . . . 4  class recs ( ( h  e.  _V  |->  (
iota_ v  e.  { w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
28 vz . . . . . . . . 9  set  z
2928cv 1618 . . . . . . . 8  class  z
30 vt . . . . . . . . 9  set  t
3130cv 1618 . . . . . . . 8  class  t
3229, 31, 2wbr 3983 . . . . . . 7  wff  z R t
33 vx . . . . . . . . 9  set  x
3433cv 1618 . . . . . . . 8  class  x
3527, 34cima 4650 . . . . . . 7  class  (recs ( ( h  e.  _V  |->  ( iota_ v  e.  {
w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x )
3632, 28, 35wral 2516 . . . . . 6  wff  A. z  e.  (recs ( ( h  e.  _V  |->  ( iota_ v  e.  { w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t
3736, 30, 1wrex 2517 . . . . 5  wff  E. t  e.  A  A. z  e.  (recs ( ( h  e.  _V  |->  ( iota_ v  e.  { w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t
38 con0 4350 . . . . 5  class  On
3937, 33, 38crab 2520 . . . 4  class  { x  e.  On  |  E. t  e.  A  A. z  e.  (recs ( ( h  e.  _V  |->  ( iota_ v  e.  { w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t }
4027, 39cres 4649 . . 3  class  (recs ( ( h  e.  _V  |->  ( iota_ v  e.  {
w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )  |`  { x  e.  On  |  E. t  e.  A  A. z  e.  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t } )
41 c0 3416 . . 3  class  (/)
426, 40, 41cif 3525 . 2  class  if ( ( R  We  A  /\  R Se  A ) ,  (recs ( ( h  e.  _V  |->  ( iota_ v  e.  { w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e.  { w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )  |`  { x  e.  On  |  E. t  e.  A  A. z  e.  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t } ) ,  (/) )
433, 42wceq 1619 1  wff OrdIso ( R ,  A )  =  if ( ( R  We  A  /\  R Se  A ) ,  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )  |`  { x  e.  On  |  E. t  e.  A  A. z  e.  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t } ) ,  (/) )
Colors of variables: wff set class
This definition is referenced by:  dfoi  7180  oieq1  7181  oieq2  7182  nfoi  7183  oi0  7197
  Copyright terms: Public domain W3C validator