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

Definition df-oi 7482
 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 7481 . 2 OrdIso
41, 2wwe 4543 . . . 4
51, 2wse 4542 . . . 4 Se
64, 5wa 360 . . 3 Se
7 vh . . . . . 6
8 cvv 2958 . . . . . 6
9 vu . . . . . . . . . . 11
109cv 1652 . . . . . . . . . 10
11 vv . . . . . . . . . . 11
1211cv 1652 . . . . . . . . . 10
1310, 12, 2wbr 4215 . . . . . . . . 9
1413wn 3 . . . . . . . 8
15 vj . . . . . . . . . . . 12
1615cv 1652 . . . . . . . . . . 11
17 vw . . . . . . . . . . . 12
1817cv 1652 . . . . . . . . . . 11
1916, 18, 2wbr 4215 . . . . . . . . . 10
207cv 1652 . . . . . . . . . . 11
2120crn 4882 . . . . . . . . . 10
2219, 15, 21wral 2707 . . . . . . . . 9
2322, 17, 1crab 2711 . . . . . . . 8
2414, 9, 23wral 2707 . . . . . . 7
2524, 11, 23crio 6545 . . . . . 6
267, 8, 25cmpt 4269 . . . . 5
2726crecs 6635 . . . 4 recs
28 vz . . . . . . . . 9
2928cv 1652 . . . . . . . 8
30 vt . . . . . . . . 9
3130cv 1652 . . . . . . . 8
3229, 31, 2wbr 4215 . . . . . . 7
33 vx . . . . . . . . 9
3433cv 1652 . . . . . . . 8
3527, 34cima 4884 . . . . . . 7 recs
3632, 28, 35wral 2707 . . . . . 6 recs
3736, 30, 1wrex 2708 . . . . 5 recs
38 con0 4584 . . . . 5
3937, 33, 38crab 2711 . . . 4 recs
4027, 39cres 4883 . . 3 recs recs
41 c0 3630 . . 3
426, 40, 41cif 3741 . 2 Se recs recs
433, 42wceq 1653 1 OrdIso Se recs recs
 Colors of variables: wff set class This definition is referenced by:  dfoi  7483  oieq1  7484  oieq2  7485  nfoi  7486  oi0  7500
 Copyright terms: Public domain W3C validator