Definition df-ord

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. (Contributed by NM, 17-Sep-1993)

	Ref	Expression
Assertion	df-ord	|- ( Ord A <-> ( Tr A /\ _E We A ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	word	|- Ord A
2	0	wtr	|- Tr A
3		cep	|- _E
4	0 3	wwe	|- _E We A
5	2 4	wa	|- ( Tr A /\ _E We A )
6	1 5	wb	|- ( Ord A <-> ( Tr A /\ _E We A ) )