![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-tr | Structured version Visualization version GIF version |
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6103). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5263 (which is suggestive of the word "transitive"), dftr2c 5264, dftr3 5267, dftr4 5268, dftr5 5265, and (when 𝐴 is a set) unisuc 6435. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
Ref | Expression |
---|---|
df-tr | ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wtr 5261 | . 2 wff Tr 𝐴 |
3 | 1 | cuni 4904 | . . 3 class ∪ 𝐴 |
4 | 3, 1 | wss 3946 | . 2 wff ∪ 𝐴 ⊆ 𝐴 |
5 | 2, 4 | wb 205 | 1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
Colors of variables: wff setvar class |
This definition is referenced by: dftr2 5263 dftr4 5268 treq 5269 trv 5275 pwtr 5448 unisucg 6434 orduniss 6453 onuninsuci 7816 trcl 9710 tc2 9724 r1tr2 9759 tskuni 10765 untangtr 34614 hfuni 35087 |
Copyright terms: Public domain | W3C validator |