Theorem brtrclfvcnv

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

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

Proof

Step	Hyp	Ref	Expression
1		cnvexg	⊢ ( 𝑅 ∈ 𝑉 → ◡ 𝑅 ∈ V )
2		brtrclfv	⊢ ( ◡ 𝑅 ∈ V → ( 𝐴 ( t+ ‘ ◡ 𝑅 ) 𝐵 ↔ ∀ 𝑟 ( ( ◡ 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐴 𝑟 𝐵 ) ) )
3	1 2	syl	⊢ ( 𝑅 ∈ 𝑉 → ( 𝐴 ( t+ ‘ ◡ 𝑅 ) 𝐵 ↔ ∀ 𝑟 ( ( ◡ 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐴 𝑟 𝐵 ) ) )