Definition df-tr 2755

Description: Define a transitive class. Not to be confused with a transitive relation (see cotr 3528). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 2756 (which is suggestive of the word "transitive"), dftr3 2758, dftr4 2759, dftr5 2757, and (when A is a set) unisuc 3049. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130.

Assertion

Ref	Expression
df-tr	⊢ (Tr A ↔ ∪A ⊆ A)

Detailed syntax breakdown of Definition df-tr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wtr 2754	. 2 wff Tr A
3	1	cuni 2569	. . 3 class ∪A
4	3, 1	wss 2099	. 2 wff ∪A ⊆ A
5	2, 4	wb 144	1 wff (Tr A ↔ ∪A ⊆ A)

This definition is referenced by:  dftr2 2756  dftr4 2759  treq 2760  trv 2766  unisuc 3049  orduniss 3066  onuninsuci 3194  trcl 4791

Copyright terms: Public domain