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 6365
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 6361 . 2 wff Ord 𝐴
31wtr 5265 . . 3 wff Tr 𝐴
4 cep 5579 . . . 4 class E
51, 4wwe 5630 . . 3 wff E We 𝐴
63, 5wa 397 . 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  6369  ordwe  6375  ordtr  6376  trssord  6379  ordelord  6384  ord0  6415  ordon  7761  dford5  7768  dfrecs3  8369  dfrecs3OLD  8370  dford2  9612  smobeth  10578  gruina  10810  dford5reg  34743  dfon2  34753  oaun3lem1  42110
  Copyright terms: Public domain W3C validator