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

Definition df-oi 7956
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
Distinct variable groups:   , , , , , , , ,   , , , , , , , ,

Detailed syntax breakdown of Definition df-oi
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2coi 7955 . 2
41, 2wwe 4842 . . . 4
51, 2wse 4841 . . . 4
64, 5wa 369 . . 3
7 vh . . . . . 6
8 cvv 3109 . . . . . 6
9 vu . . . . . . . . . . 11
109cv 1394 . . . . . . . . . 10
11 vv . . . . . . . . . . 11
1211cv 1394 . . . . . . . . . 10
1310, 12, 2wbr 4452 . . . . . . . . 9
1413wn 3 . . . . . . . 8
15 vj . . . . . . . . . . . 12
1615cv 1394 . . . . . . . . . . 11
17 vw . . . . . . . . . . . 12
1817cv 1394 . . . . . . . . . . 11
1916, 18, 2wbr 4452 . . . . . . . . . 10
207cv 1394 . . . . . . . . . . 11
2120crn 5005 . . . . . . . . . 10
2219, 15, 21wral 2807 . . . . . . . . 9
2322, 17, 1crab 2811 . . . . . . . 8
2414, 9, 23wral 2807 . . . . . . 7
2524, 11, 23crio 6256 . . . . . 6
267, 8, 25cmpt 4510 . . . . 5
2726crecs 7060 . . . 4
28 vz . . . . . . . . 9
2928cv 1394 . . . . . . . 8
30 vt . . . . . . . . 9
3130cv 1394 . . . . . . . 8
3229, 31, 2wbr 4452 . . . . . . 7
33 vx . . . . . . . . 9
3433cv 1394 . . . . . . . 8
3527, 34cima 5007 . . . . . . 7
3632, 28, 35wral 2807 . . . . . 6
3736, 30, 1wrex 2808 . . . . 5
38 con0 4883 . . . . 5
3937, 33, 38crab 2811 . . . 4
4027, 39cres 5006 . . 3
41 c0 3784 . . 3
426, 40, 41cif 3941 . 2
433, 42wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  dfoi  7957  oieq1  7958  oieq2  7959  nfoi  7960  oi0  7974
  Copyright terms: Public domain W3C validator