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 6385
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 6381 . 2 wff Ord 𝐴
31wtr 5257 . . 3 wff Tr 𝐴
4 cep 5581 . . . 4 class E
51, 4wwe 5634 . . 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  6389  ordwe  6395  ordtr  6396  trssord  6399  ordelord  6404  ord0  6435  ordon  7793  dford5  7800  dfrecs3  8408  dfrecs3OLD  8409  dford2  9656  smobeth  10622  gruina  10854  dford5reg  35761  dfon2  35771  oaun3lem1  43365
  Copyright terms: Public domain W3C validator