This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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++ 𝑅 = ∩ { 𝑧 ∣ ( 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )