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 14696
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 14694 . 2 class t+
2 vx . . 3 setvar 𝑥
3 cvv 3431 . . 3 class V
42cv 1541 . . . . . . 7 class 𝑥
5 vz . . . . . . . 8 setvar 𝑧
65cv 1541 . . . . . . 7 class 𝑧
74, 6wss 3892 . . . . . 6 wff 𝑥𝑧
86, 6ccom 5594 . . . . . . 7 class (𝑧𝑧)
98, 6wss 3892 . . . . . 6 wff (𝑧𝑧) ⊆ 𝑧
107, 9wa 396 . . . . 5 wff (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)
1110, 5cab 2717 . . . 4 class {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)}
1211cint 4885 . . 3 class {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)}
132, 3, 12cmpt 5162 . 2 class (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
141, 13wceq 1542 1 wff t+ = (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
Colors of variables: wff setvar class
This definition is referenced by:  trclfv  14709  dftrcl3  41298
  Copyright terms: Public domain W3C validator