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 ⊢ B R ↾ A C ↔ B R ∩ A × ran ⁡ R ↾ A C

Proof

Step Hyp Ref Expression
1 brres ⊢ C ∈ ran ⁡ R ↾ A → B R ↾ A C ↔ B ∈ A ∧ B R C
2 1 pm5.32i ⊢ C ∈ ran ⁡ R ↾ A ∧ B R ↾ A C ↔ C ∈ ran ⁡ R ↾ A ∧ B ∈ A ∧ B R C
3 relres ⊢ Rel ⁡ R ↾ A
4 3 relelrni ⊢ B R ↾ A C → C ∈ ran ⁡ R ↾ A
5 4 pm4.71ri ⊢ B R ↾ A C ↔ C ∈ ran ⁡ R ↾ A ∧ B R ↾ A C
6 brinxp2 ⊢ B R ∩ A × ran ⁡ R ↾ A C ↔ B ∈ A ∧ C ∈ ran ⁡ R ↾ A ∧ B R C
7 df-3an ⊢ B ∈ A ∧ C ∈ ran ⁡ R ↾ A ∧ B R C ↔ B ∈ A ∧ C ∈ ran ⁡ R ↾ A ∧ B R C
8 3anan12 ⊢ B ∈ A ∧ C ∈ ran ⁡ R ↾ A ∧ B R C ↔ C ∈ ran ⁡ R ↾ A ∧ B ∈ A ∧ B R C
9 6 7 8 3bitr2i ⊢ B R ∩ A × ran ⁡ R ↾ A C ↔ C ∈ ran ⁡ R ↾ A ∧ B ∈ A ∧ B R C
10 2 5 9 3bitr4i ⊢ B R ↾ A C ↔ B R ∩ A × ran ⁡ R ↾ A C