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

Definition df-oi 7222
 Description: Define the canonical order isomorphism from the well-order on to an ordinal. (Contributed by Mario Carneiro, 23-May-2015.)
Assertion
Ref Expression
df-oi OrdIso Se recs recs
Distinct variable groups:   ,,,,,,,,   ,,,,,,,,

Detailed syntax breakdown of Definition df-oi
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2coi 7221 . 2 OrdIso
41, 2wwe 4352 . . . 4
51, 2wse 4351 . . . 4 Se
64, 5wa 360 . . 3 Se
7 vh . . . . . 6
8 cvv 2791 . . . . . 6
9 vu . . . . . . . . . . 11
109cv 1624 . . . . . . . . . 10
11 vv . . . . . . . . . . 11
1211cv 1624 . . . . . . . . . 10
1310, 12, 2wbr 4026 . . . . . . . . 9
1413wn 5 . . . . . . . 8
15 vj . . . . . . . . . . . 12
1615cv 1624 . . . . . . . . . . 11
17 vw . . . . . . . . . . . 12
1817cv 1624 . . . . . . . . . . 11
1916, 18, 2wbr 4026 . . . . . . . . . 10
207cv 1624 . . . . . . . . . . 11
2120crn 4691 . . . . . . . . . 10
2219, 15, 21wral 2546 . . . . . . . . 9
2322, 17, 1crab 2550 . . . . . . . 8
2414, 9, 23wral 2546 . . . . . . 7
2524, 11, 23crio 6292 . . . . . 6
267, 8, 25cmpt 4080 . . . . 5
2726crecs 6384 . . . 4 recs
28 vz . . . . . . . . 9
2928cv 1624 . . . . . . . 8
30 vt . . . . . . . . 9
3130cv 1624 . . . . . . . 8
3229, 31, 2wbr 4026 . . . . . . 7
33 vx . . . . . . . . 9
3433cv 1624 . . . . . . . 8
3527, 34cima 4693 . . . . . . 7 recs
3632, 28, 35wral 2546 . . . . . 6 recs
3736, 30, 1wrex 2547 . . . . 5 recs
38 con0 4393 . . . . 5
3937, 33, 38crab 2550 . . . 4 recs
4027, 39cres 4692 . . 3 recs recs
41 c0 3458 . . 3
426, 40, 41cif 3568 . 2 Se recs recs
433, 42wceq 1625 1 OrdIso Se recs recs
 Colors of variables: wff set class This definition is referenced by:  dfoi  7223  oieq1  7224  oieq2  7225  nfoi  7226  oi0  7240
 Copyright terms: Public domain W3C validator