Definition df-iord 4121

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". (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4122 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 4117	. 2 wff Ord A
3	1	wtr 3875	. . 3 wff Tr A
4		vx	. . . . . 6 setvar x
5	4	cv 1283	. . . . 5 class x
6	5	wtr 3875	. . . 4 wff Tr x
7	6, 4, 1	wral 2348	. . 3 wff A. x e. A Tr x
8	3, 7	wa 102	. 2 wff ( Tr A /\ A. x e. A Tr x )
9	2, 8	wb 103	1 wff ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )

This definition is referenced by:  dford3  4122