Definition df-trcl

Description: Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011)

	Ref	Expression
Assertion	df-trcl	⊢ t+ = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctcl	⊢ t+
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vz	⊢ 𝑧
4	1	cv	⊢ 𝑥
5	3	cv	⊢ 𝑧
6	4 5	wss	⊢ 𝑥 ⊆ 𝑧
7	5 5	ccom	⊢ ( 𝑧 ∘ 𝑧 )
8	7 5	wss	⊢ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧
9	6 8	wa	⊢ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 )
10	9 3	cab	⊢ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) }
11	10	cint	⊢ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) }
12	1 2 11	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
13	0 12	wceq	⊢ t+ = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )