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 6378
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 6374 . 2 wff Ord 𝐴
31wtr 5263 . . 3 wff Tr 𝐴
4 cep 5577 . . . 4 class E
51, 4wwe 5629 . . 3 wff E We 𝐴
63, 5wa 395 . 2 wff (Tr 𝐴 ∧ E We 𝐴)
72, 6wb 206 1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  ordeq  6382  ordwe  6388  ordtr  6389  trssord  6392  ordelord  6397  ord0  6428  ordon  7783  dford5  7790  dfrecs3  8398  dfrecs3OLD  8399  dford2  9644  smobeth  10610  gruina  10842  dford5reg  35719  dfon2  35729  oaun3lem1  43323
  Copyright terms: Public domain W3C validator