MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-trcl Structured version   Visualization version   GIF version

Definition df-trcl 13523
Description: Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011.)
Assertion
Ref Expression
df-trcl t+ = (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
Distinct variable group:   𝑥,𝑧

Detailed syntax breakdown of Definition df-trcl
StepHypRef Expression
1 ctcl 13521 . 2 class t+
2 vx . . 3 setvar 𝑥
3 cvv 3173 . . 3 class V
42cv 1474 . . . . . . 7 class 𝑥
5 vz . . . . . . . 8 setvar 𝑧
65cv 1474 . . . . . . 7 class 𝑧
74, 6wss 3540 . . . . . 6 wff 𝑥𝑧
86, 6ccom 5032 . . . . . . 7 class (𝑧𝑧)
98, 6wss 3540 . . . . . 6 wff (𝑧𝑧) ⊆ 𝑧
107, 9wa 383 . . . . 5 wff (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)
1110, 5cab 2596 . . . 4 class {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)}
1211cint 4405 . . 3 class {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)}
132, 3, 12cmpt 4638 . 2 class (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
141, 13wceq 1475 1 wff t+ = (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
Colors of variables: wff setvar class
This definition is referenced by:  trclfv  13538  dftrcl3  36825
  Copyright terms: Public domain W3C validator