Definition df-oi 8415

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	coi 8414	. 2 class OrdIso ( R , A )
4	1, 2	wwe 5072	. . . 4 wff R We A
5	1, 2	wse 5071	. . . 4 wff R Se A
6	4, 5	wa 384	. . 3 wff ( R We A /\ R Se A )
7		vh	. . . . . 6 setvar h
8		cvv 3200	. . . . . 6 class _V
9		vu	. . . . . . . . . . 11 setvar u
10	9	cv 1482	. . . . . . . . . 10 class u
11		vv	. . . . . . . . . . 11 setvar v
12	11	cv 1482	. . . . . . . . . 10 class v
13	10, 12, 2	wbr 4653	. . . . . . . . 9 wff u R v
14	13	wn 3	. . . . . . . 8 wff -. u R v
15		vj	. . . . . . . . . . . 12 setvar j
16	15	cv 1482	. . . . . . . . . . 11 class j
17		vw	. . . . . . . . . . . 12 setvar w
18	17	cv 1482	. . . . . . . . . . 11 class w
19	16, 18, 2	wbr 4653	. . . . . . . . . 10 wff j R w
20	7	cv 1482	. . . . . . . . . . 11 class h
21	20	crn 5115	. . . . . . . . . 10 class ran h
22	19, 15, 21	wral 2912	. . . . . . . . 9 wff A. j e. ran h j R w
23	22, 17, 1	crab 2916	. . . . . . . 8 class { w e. A | A. j e. ran h j R w }
24	14, 9, 23	wral 2912	. . . . . . 7 wff A. u e. { w e. A | A. j e. ran h j R w } -. u R v
25	24, 11, 23	crio 6610	. . . . . 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 )
26	7, 8, 25	cmpt 4729	. . . . 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 ) )
27	26	crecs 7467	. . . 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 setvar z
29	28	cv 1482	. . . . . . . 8 class z
30		vt	. . . . . . . . 9 setvar t
31	30	cv 1482	. . . . . . . 8 class t
32	29, 31, 2	wbr 4653	. . . . . . 7 wff z R t
33		vx	. . . . . . . . 9 setvar x
34	33	cv 1482	. . . . . . . 8 class x
35	27, 34	cima 5117	. . . . . . 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 )
36	32, 28, 35	wral 2912	. . . . . 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
37	36, 30, 1	wrex 2913	. . . . 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 5723	. . . . 5 class On
39	37, 33, 38	crab 2916	. . . 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 }
40	27, 39	cres 5116	. . 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 3915	. . 3 class (/)
42	6, 40, 41	cif 4086	. 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 } ) , (/) )
43	3, 42	wceq 1483	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 } ) , (/) )

This definition is referenced by:  dfoi  8416  oieq1  8417  oieq2  8418  nfoi  8419  oi0  8433