Definition df-trcl 14341

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 14339	. 2 class t+
2		vx	. . 3 setvar 𝑥
3		cvv 3495	. . 3 class V
4	2	cv 1532	. . . . . . 7 class 𝑥
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1532	. . . . . . 7 class 𝑧
7	4, 6	wss 3936	. . . . . 6 wff 𝑥 ⊆ 𝑧
8	6, 6	ccom 5554	. . . . . . 7 class (𝑧 ∘ 𝑧)
9	8, 6	wss 3936	. . . . . 6 wff (𝑧 ∘ 𝑧) ⊆ 𝑧
10	7, 9	wa 398	. . . . 5 wff (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)
11	10, 5	cab 2799	. . . 4 class {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
12	11	cint 4869	. . 3 class ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}
13	2, 3, 12	cmpt 5139	. 2 class (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
14	1, 13	wceq 1533	1 wff t+ = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})

This definition is referenced by:  trclfv  14354  dftrcl3  40058