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 6379
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 6375 . 2 wff Ord 𝐴
31wtr 5270 . . 3 wff Tr 𝐴
4 cep 5585 . . . 4 class E
51, 4wwe 5636 . . 3 wff E We 𝐴
63, 5wa 394 . 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  6383  ordwe  6389  ordtr  6390  trssord  6393  ordelord  6398  ord0  6429  ordon  7785  dford5  7792  dfrecs3  8402  dfrecs3OLD  8403  dford2  9663  smobeth  10629  gruina  10861  dford5reg  35606  dfon2  35616  oaun3lem1  43040
  Copyright terms: Public domain W3C validator