Theorem cotrtrclfv

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

	Ref	Expression
Assertion	cotrtrclfv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ( t+ ‘ 𝑅 ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		trclfv	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
2	1	adantr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ( t+ ‘ 𝑅 ) = ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
3		simpr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
4		ssid	⊢ 𝑅 ⊆ 𝑅
5	3 4	jctil	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ( 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) )
6		trcleq2lem	⊢ ( 𝑟 = 𝑅 → ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ) )
7	6	elabg	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ↔ ( 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ) )
8	7	adantr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ( 𝑅 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ↔ ( 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ) )
9	5 8	mpbird	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → 𝑅 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
10		intss1	⊢ ( 𝑅 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ⊆ 𝑅 )
11	9 10	syl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ⊆ 𝑅 )
12	2 11	eqsstrd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ( t+ ‘ 𝑅 ) ⊆ 𝑅 )
13		trclfvlb	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
14	13	adantr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
15	12 14	eqssd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) → ( t+ ‘ 𝑅 ) = 𝑅 )