Metamath Proof Explorer

Definition df-oi

Description: Define the canonical order isomorphism from the well-order R on A to an ordinal. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Assertion 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 } ) , (/) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 cA 
 |-  A
2 1 0 coi 
 |-  OrdIso ( R , A )
3 1 0 wwe 
 |-  R We A
4 1 0 wse 
 |-  R Se A
5 3 4 wa 
 |-  ( R We A /\ R Se A )
6 vh 
 |-  h
7 cvv 
 |-  _V
8 vv 
 |-  v
9 vw 
 |-  w
10 vj 
 |-  j
11 6 cv 
 |-  h
12 11 crn 
 |-  ran h
13 10 cv 
 |-  j
14 9 cv 
 |-  w
15 13 14 0 wbr 
 |-  j R w
16 15 10 12 wral 
 |-  A. j e. ran h j R w
17 16 9 1 crab 
 |-  { w e. A | A. j e. ran h j R w }
18 vu 
 |-  u
19 18 cv 
 |-  u
20 8 cv 
 |-  v
21 19 20 0 wbr 
 |-  u R v
22 21 wn 
 |-  -. u R v
23 22 18 17 wral 
 |-  A. u e. { w e. A | A. j e. ran h j R w } -. u R v
24 23 8 17 crio 
 |-  ( 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 )
25 6 7 24 cmpt 
 |-  ( 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 ) )
26 25 crecs 
 |-  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 ) ) )
27 vx 
 |-  x
28 con0 
 |-  On
29 vt 
 |-  t
30 vz 
 |-  z
31 27 cv 
 |-  x
32 26 31 cima 
 |-  ( 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 )
33 30 cv 
 |-  z
34 29 cv 
 |-  t
35 33 34 0 wbr 
 |-  z R t
36 35 30 32 wral 
 |-  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
37 36 29 1 wrex 
 |-  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 37 27 28 crab 
 |-  { 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 }
39 26 38 cres 
 |-  ( 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 } )
40 c0 
 |-  (/)
41 5 39 40 cif 
 |-  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 } ) , (/) )
42 2 41 wceq 
 |-  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 } ) , (/) )