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 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	word	⊢ Ord 𝐴
2	0	wtr	⊢ Tr 𝐴
3		cep	⊢ E
4	0 3	wwe	⊢ E We 𝐴
5	2 4	wa	⊢ ( Tr 𝐴 ∧ E We 𝐴 )
6	1 5	wb	⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) )