Definition df-trcl 15120

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 15118	. 2 class t+
2		vx	. . 3 setvar 𝑥
3		cvv 3451	. . 3 class V
4	2	cv 1569	. . . . . . 7 class 𝑥
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1569	. . . . . . 7 class 𝑧
7	4, 6	wss 3899	. . . . . 6 wff 𝑥 ⊆ 𝑧
8	6, 6	ccom 5655	. . . . . . 7 class (𝑧 ∘ 𝑧)
9	8, 6	wss 3899	. . . . . 6 wff (𝑧 ∘ 𝑧) ⊆ 𝑧
10	7, 9	wa 401	. . . . 5 wff (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)
11	10, 5	cab 2739	. . . 4 class {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
12	11	cint 4907	. . 3 class ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
13	2, 3, 12	cmpt 5186	. 2 class (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
14	1, 13	wceq 1570	1 wff t+ = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})

This definition is used by:  trclfv  15133  dftrcl3  44679