Metamath Proof Explorer

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.

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

(Contributed by NM, 17-Sep-1993)

		Ref	Expression
	Assertion	df-ord	$⊢ Ord A \leftrightarrow (Tr A \land E We A)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1	0	word	$wff Ord A$
2	0	wtr	$wff Tr A$
3		cep	$class E$
4	0 3	wwe	$wff E We A$
5	2 4	wa	$wff (Tr A \land E We A)$
6	1 5	wb	$wff (Ord A \leftrightarrow (Tr A \land E We A))$