Definition df-ord 6380

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 6376	. 2 wff Ord 𝐴
3	1	wtr 5215	. . 3 wff Tr 𝐴
4		cep 5554	. . . 4 class E
5	1, 4	wwe 5607	. . 3 wff E We 𝐴
6	3, 5	wa 401	. 2 wff (Tr 𝐴 ∧ E We 𝐴)
7	2, 6	wb 209	1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))

This definition is used by:  ordeq  6384  ordwe  6390  ordtr  6391  trssord  6394  ordelord  6399  ord0  6432  ordon  7812  dford5  7819  dfrecs3  8405  dford2  9645  smobeth  10695  gruina  10927  onprcr  36630  dford5reg  36721  dfon2  36731  oaun3lem1  44566