Theorem brtrclfv

Description: Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020)

	Ref	Expression
Assertion	brtrclfv	⊢ ( 𝑅 ∈ 𝑉 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐴 𝑟 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		trclfv	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
2	1	breqd	⊢ ( 𝑅 ∈ 𝑉 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ↔ 𝐴 ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝐵 ) )
3		brintclab	⊢ ( 𝐴 ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝐵 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
4		df-br	⊢ ( 𝐴 𝑟 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 )
5	4	imbi2i	⊢ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐴 𝑟 𝐵 ) ↔ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
6	5	albii	⊢ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐴 𝑟 𝐵 ) ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
7	3 6	bitr4i	⊢ ( 𝐴 ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝐵 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐴 𝑟 𝐵 ) )
8	2 7	bitrdi	⊢ ( 𝑅 ∈ 𝑉 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐴 𝑟 𝐵 ) ) )