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 ( 𝑅 ↾ 𝐴 ) ) ) 𝐶 )