Metamath Proof Explorer


Theorem trclfv

Description: The transitive closure of a relation. (Contributed by RP, 28-Apr-2020)

Ref Expression
Assertion trclfv ( 𝑅𝑉 → ( t+ ‘ 𝑅 ) = { 𝑥 ∣ ( 𝑅𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 elex ( 𝑅𝑉𝑅 ∈ V )
2 trclexlem ( 𝑅 ∈ V → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ V )
3 trclubg ( 𝑅 ∈ V → { 𝑥 ∣ ( 𝑅𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
4 2 3 ssexd ( 𝑅 ∈ V → { 𝑥 ∣ ( 𝑅𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } ∈ V )
5 trcleq1 ( 𝑟 = 𝑅 { 𝑥 ∣ ( 𝑟𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } = { 𝑥 ∣ ( 𝑅𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } )
6 df-trcl t+ = ( 𝑟 ∈ V ↦ { 𝑥 ∣ ( 𝑟𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } )
7 5 6 fvmptg ( ( 𝑅 ∈ V ∧ { 𝑥 ∣ ( 𝑅𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } ∈ V ) → ( t+ ‘ 𝑅 ) = { 𝑥 ∣ ( 𝑅𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } )
8 1 4 7 syl2anc2 ( 𝑅𝑉 → ( t+ ‘ 𝑅 ) = { 𝑥 ∣ ( 𝑅𝑥 ∧ ( 𝑥𝑥 ) ⊆ 𝑥 ) } )