Theorem dfttrcl2

Description: When R is a set and a relation, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Assertion	dfttrcl2	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → t++ 𝑅 = ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )

Proof

Step	Hyp	Ref	Expression
1		ssintab	⊢ ( t++ 𝑅 ⊆ ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ∀ 𝑧 ( ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) → t++ 𝑅 ⊆ 𝑧 ) )
2		ttrclss	⊢ ( ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) → t++ 𝑅 ⊆ 𝑧 )
3	1 2	mpgbir	⊢ t++ 𝑅 ⊆ ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) }
4	3	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → t++ 𝑅 ⊆ ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
5		rabab	⊢ { 𝑧 ∈ V ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) }
6	5	inteqi	⊢ ∩ { 𝑧 ∈ V ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) }
7		ttrclexg	⊢ ( 𝑅 ∈ 𝑉 → t++ 𝑅 ∈ V )
8		ssttrcl	⊢ ( Rel 𝑅 → 𝑅 ⊆ t++ 𝑅 )
9		ttrcltr	⊢ ( t++ 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅
10	8 9	jctir	⊢ ( Rel 𝑅 → ( 𝑅 ⊆ t++ 𝑅 ∧ ( t++ 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅 ) )
11		sseq2	⊢ ( 𝑧 = t++ 𝑅 → ( 𝑅 ⊆ 𝑧 ↔ 𝑅 ⊆ t++ 𝑅 ) )
12		coeq1	⊢ ( 𝑧 = t++ 𝑅 → ( 𝑧 ∘ 𝑧 ) = ( t++ 𝑅 ∘ 𝑧 ) )
13		coeq2	⊢ ( 𝑧 = t++ 𝑅 → ( t++ 𝑅 ∘ 𝑧 ) = ( t++ 𝑅 ∘ t++ 𝑅 ) )
14	12 13	eqtrd	⊢ ( 𝑧 = t++ 𝑅 → ( 𝑧 ∘ 𝑧 ) = ( t++ 𝑅 ∘ t++ 𝑅 ) )
15		id	⊢ ( 𝑧 = t++ 𝑅 → 𝑧 = t++ 𝑅 )
16	14 15	sseq12d	⊢ ( 𝑧 = t++ 𝑅 → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( t++ 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅 ) )
17	11 16	anbi12d	⊢ ( 𝑧 = t++ 𝑅 → ( ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( 𝑅 ⊆ t++ 𝑅 ∧ ( t++ 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅 ) ) )
18	17	intminss	⊢ ( ( t++ 𝑅 ∈ V ∧ ( 𝑅 ⊆ t++ 𝑅 ∧ ( t++ 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅 ) ) → ∩ { 𝑧 ∈ V ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ t++ 𝑅 )
19	7 10 18	syl2an	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ∩ { 𝑧 ∈ V ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ t++ 𝑅 )
20	6 19	eqsstrrid	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ t++ 𝑅 )
21	4 20	eqssd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → t++ 𝑅 = ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )