Definition df-ord 6368

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 6364	. 2 wff Ord 𝐴
3	1	wtr 5266	. . 3 wff Tr 𝐴
4		cep 5580	. . . 4 class E
5	1, 4	wwe 5631	. . 3 wff E We 𝐴
6	3, 5	wa 397	. 2 wff (Tr 𝐴 ∧ E We 𝐴)
7	2, 6	wb 205	1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))

This definition is referenced by:  ordeq  6372  ordwe  6378  ordtr  6379  trssord  6382  ordelord  6387  ord0  6418  ordon  7764  dford5  7771  dfrecs3  8372  dfrecs3OLD  8373  dford2  9615  smobeth  10581  gruina  10813  dford5reg  34785  dfon2  34795  oaun3lem1  42172