Definition df-ord 3814

Description: Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the epsilon relation. Variant of definition of [BellMachover] p. 468.

Assertion

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

Detailed syntax breakdown of Definition df-ord

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	word 3810	. 2 wff Ord A
3	1	wtr 3579	. . 3 wff Tr A
4		cep 3742	. . . 4 class _E
5	1, 4	wwe 3781	. . 3 wff _E We A
6	3, 5	wa 337	. 2 wff (Tr A /\ _E We A)
7	2, 6	wb 219	1 wff (Ord A <-> (Tr A /\ _E We A))

This definition is referenced by:  ordeq 3818  ordwe 3824  ordtr 3825  trssord 3828  ordelord 3833  ord0 3862  ordon 4008  dford2 5943  dford3 14482  dfon2 14492  tfrALTlem 14629  tartord 16050

Copyright terms: Public domain