Theorem brcnvtrclfv

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

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

Proof

Step	Hyp	Ref	Expression
1		brcnvg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ◡ ( t+ ‘ 𝑅 ) 𝐵 ↔ 𝐵 ( t+ ‘ 𝑅 ) 𝐴 ) )
2	1	3adant1	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ◡ ( t+ ‘ 𝑅 ) 𝐵 ↔ 𝐵 ( t+ ‘ 𝑅 ) 𝐴 ) )
3		brtrclfv	⊢ ( 𝑅 ∈ 𝑈 → ( 𝐵 ( t+ ‘ 𝑅 ) 𝐴 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐵 𝑟 𝐴 ) ) )
4	3	3ad2ant1	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ( t+ ‘ 𝑅 ) 𝐴 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐵 𝑟 𝐴 ) ) )
5	2 4	bitrd	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ◡ ( t+ ‘ 𝑅 ) 𝐵 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝐵 𝑟 𝐴 ) ) )