Definition df-ord 6393

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 6389	. 2 wff Ord 𝐴
3	1	wtr 5283	. . 3 wff Tr 𝐴
4		cep 5598	. . . 4 class E
5	1, 4	wwe 5649	. . 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  6397  ordwe  6403  ordtr  6404  trssord  6407  ordelord  6412  ord0  6443  ordon  7806  dford5  7813  dfrecs3  8422  dfrecs3OLD  8423  dford2  9683  smobeth  10649  gruina  10881  dford5reg  35738  dfon2  35748  oaun3lem1  43331