MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ord Structured version   Visualization version   GIF version

Definition df-ord 6273
Description: Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the membership relation. Variant of definition of [BellMachover] p. 468.

Some sources will define a notation for ordinal order corresponding to < and but we just use and respectively.

(Contributed by NM, 17-Sep-1993.)

Assertion
Ref Expression
df-ord (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))

Detailed syntax breakdown of Definition df-ord
StepHypRef Expression
1 cA . . 3 class 𝐴
21word 6269 . 2 wff Ord 𝐴
31wtr 5192 . . 3 wff Tr 𝐴
4 cep 5495 . . . 4 class E
51, 4wwe 5544 . . 3 wff E We 𝐴
63, 5wa 396 . 2 wff (Tr 𝐴 ∧ E We 𝐴)
72, 6wb 205 1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  ordeq  6277  ordwe  6283  ordtr  6284  trssord  6287  ordelord  6292  ord0  6322  ordon  7636  dfrecs3  8212  dfrecs3OLD  8213  dford2  9387  smobeth  10351  gruina  10583  dford5  33680  dford5reg  33767  dfon2  33777
  Copyright terms: Public domain W3C validator