Definition df-trcl 13574

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 13572	. 2 class t+
2		vx	. . 3 setvar 𝑥
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . . . 7 class 𝑥
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1474	. . . . . . 7 class 𝑧
7	4, 6	wss 3540	. . . . . 6 wff 𝑥 ⊆ 𝑧
8	6, 6	ccom 5042	. . . . . . 7 class (𝑧 ∘ 𝑧)
9	8, 6	wss 3540	. . . . . 6 wff (𝑧 ∘ 𝑧) ⊆ 𝑧
10	7, 9	wa 383	. . . . 5 wff (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)
11	10, 5	cab 2596	. . . 4 class {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
12	11	cint 4410	. . 3 class ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
13	2, 3, 12	cmpt 4643	. 2 class (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
14	1, 13	wceq 1475	1 wff t+ = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})

This definition is referenced by:  trclfv  13589  dftrcl3  37031