Definition df-trcl 14626

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

Step	Hyp	Ref	Expression
1		ctcl 14624	. 2 class t+
2		vx	. . 3 setvar 𝑥
3		cvv 3422	. . 3 class V
4	2	cv 1538	. . . . . . 7 class 𝑥
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1538	. . . . . . 7 class 𝑧
7	4, 6	wss 3883	. . . . . 6 wff 𝑥 ⊆ 𝑧
8	6, 6	ccom 5584	. . . . . . 7 class (𝑧 ∘ 𝑧)
9	8, 6	wss 3883	. . . . . 6 wff (𝑧 ∘ 𝑧) ⊆ 𝑧
10	7, 9	wa 395	. . . . 5 wff (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)
11	10, 5	cab 2715	. . . 4 class {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
12	11	cint 4876	. . 3 class ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
13	2, 3, 12	cmpt 5153	. 2 class (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
14	1, 13	wceq 1539	1 wff t+ = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})

This definition is referenced by:  trclfv  14639  dftrcl3  41217