Theorem brcnvtrclfvcnv

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

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

Proof

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