Definition df-ord 6355

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	word 6351	. 2 wff Ord 𝐴
3	1	wtr 5229	. . 3 wff Tr 𝐴
4		cep 5552	. . . 4 class E
5	1, 4	wwe 5605	. . 3 wff E We 𝐴
6	3, 5	wa 395	. 2 wff (Tr 𝐴 ∧ E We 𝐴)
7	2, 6	wb 206	1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))

This definition is referenced by:  ordeq  6359  ordwe  6365  ordtr  6366  trssord  6369  ordelord  6374  ord0  6406  ordon  7769  dford5  7776  dfrecs3  8384  dfrecs3OLD  8385  dford2  9632  smobeth  10598  gruina  10830  dford5reg  35746  dfon2  35756  oaun3lem1  43345