This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem br1cnvres

Description: Binary relation on the converse of a restriction. (Contributed by Peter Mazsa, 27-Jul-2019)

Ref Expression
Assertion br1cnvres ( 𝐵 ∈ 𝑉 → ( 𝐵 ◡ ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × V ) )
2 1 cnveqi ⊢ ◡ ( 𝑅 ↾ 𝐴 ) = ◡ ( 𝑅 ∩ ( 𝐴 × V ) )
3 2 breqi ⊢ ( 𝐵 ◡ ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ 𝐵 ◡ ( 𝑅 ∩ ( 𝐴 × V ) ) 𝐶 )
4 elex ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
5 br1cnvinxp ⊢ ( 𝐵 ◡ ( 𝑅 ∩ ( 𝐴 × V ) ) 𝐶 ↔ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ 𝐴 ) ∧ 𝐶 𝑅 𝐵 ) )
6 anass ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐶 ∈ 𝐴 ) ∧ 𝐶 𝑅 𝐵 ) ↔ ( 𝐵 ∈ V ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 𝐵 ) ) )
7 5 6 bitri ⊢ ( 𝐵 ◡ ( 𝑅 ∩ ( 𝐴 × V ) ) 𝐶 ↔ ( 𝐵 ∈ V ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 𝐵 ) ) )
8 7 baib ⊢ ( 𝐵 ∈ V → ( 𝐵 ◡ ( 𝑅 ∩ ( 𝐴 × V ) ) 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 𝐵 ) ) )
9 4 8 syl ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ◡ ( 𝑅 ∩ ( 𝐴 × V ) ) 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 𝐵 ) ) )
10 3 9 bitrid ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ◡ ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 𝐵 ) ) )