Definition df-iord 4401

Description: Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

Some sources will define a notation for ordinal order corresponding to < and <_ but we just use e. and C_ respectively.

(Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4402 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

Ref	Expression
df-iord	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )

Distinct variable group:   x, A

Detailed syntax breakdown of Definition df-iord

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	word 4397	. 2 wff Ord A
3	1	wtr 4131	. . 3 wff Tr A
4		vx	. . . . . 6 setvar x
5	4	cv 1363	. . . . 5 class x
6	5	wtr 4131	. . . 4 wff Tr x
7	6, 4, 1	wral 2475	. . 3 wff A. x e. A Tr x
8	3, 7	wa 104	. 2 wff ( Tr A /\ A. x e. A Tr x )
9	2, 8	wb 105	1 wff ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )

This definition is referenced by:  dford3  4402