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

Metamath Proof Explorer

Theorem brres2

Description: Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019) (Revised by Peter Mazsa, 16-Dec-2021)

Ref Expression
Assertion brres2 ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ 𝐵 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝐶 )

Proof

Step Hyp Ref Expression
1 brres ⊢ ( 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) → ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )
2 1 pm5.32i ⊢ ( ( 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ) ↔ ( 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )
3 relres ⊢ Rel ( 𝑅 ↾ 𝐴 )
4 3 relelrni ⊢ ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 → 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) )
5 4 pm4.71ri ⊢ ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ ( 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ) )
6 brinxp2 ⊢ ( 𝐵 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝐶 ↔ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ) ∧ 𝐵 𝑅 𝐶 ) )
7 df-3an ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 𝑅 𝐶 ) ↔ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ) ∧ 𝐵 𝑅 𝐶 ) )
8 3anan12 ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 𝑅 𝐶 ) ↔ ( 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )
9 6 7 8 3bitr2i ⊢ ( 𝐵 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝐶 ↔ ( 𝐶 ∈ ran ( 𝑅 ↾ 𝐴 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )
10 2 5 9 3bitr4i ⊢ ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ 𝐵 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝐶 )