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 13936
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 13934 . 2 class t+
2 vx . . 3 setvar 𝑥
3 cvv 3351 . . 3 class V
42cv 1630 . . . . . . 7 class 𝑥
5 vz . . . . . . . 8 setvar 𝑧
65cv 1630 . . . . . . 7 class 𝑧
74, 6wss 3723 . . . . . 6 wff 𝑥𝑧
86, 6ccom 5254 . . . . . . 7 class (𝑧𝑧)
98, 6wss 3723 . . . . . 6 wff (𝑧𝑧) ⊆ 𝑧
107, 9wa 382 . . . . 5 wff (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)
1110, 5cab 2757 . . . 4 class {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)}
1211cint 4612 . . 3 class {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)}
132, 3, 12cmpt 4864 . 2 class (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
141, 13wceq 1631 1 wff t+ = (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
Colors of variables: wff setvar class
This definition is referenced by:  trclfv  13949  dftrcl3  38538
  Copyright terms: Public domain W3C validator