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 
|- ( B ( R |` A ) C <-> B ( R i^i ( A X. ran ( R |` A ) ) ) C )

Proof

Step Hyp Ref Expression
1 brres 
 |-  ( C e. ran ( R |` A ) -> ( B ( R |` A ) C <-> ( B e. A /\ B R C ) ) )
2 1 pm5.32i 
 |-  ( ( C e. ran ( R |` A ) /\ B ( R |` A ) C ) <-> ( C e. ran ( R |` A ) /\ ( B e. A /\ B R C ) ) )
3 relres 
 |-  Rel ( R |` A )
4 3 relelrni 
 |-  ( B ( R |` A ) C -> C e. ran ( R |` A ) )
5 4 pm4.71ri 
 |-  ( B ( R |` A ) C <-> ( C e. ran ( R |` A ) /\ B ( R |` A ) C ) )
6 brinxp2 
 |-  ( B ( R i^i ( A X. ran ( R |` A ) ) ) C <-> ( ( B e. A /\ C e. ran ( R |` A ) ) /\ B R C ) )
7 df-3an 
 |-  ( ( B e. A /\ C e. ran ( R |` A ) /\ B R C ) <-> ( ( B e. A /\ C e. ran ( R |` A ) ) /\ B R C ) )
8 3anan12 
 |-  ( ( B e. A /\ C e. ran ( R |` A ) /\ B R C ) <-> ( C e. ran ( R |` A ) /\ ( B e. A /\ B R C ) ) )
9 6 7 8 3bitr2i 
 |-  ( B ( R i^i ( A X. ran ( R |` A ) ) ) C <-> ( C e. ran ( R |` A ) /\ ( B e. A /\ B R C ) ) )
10 2 5 9 3bitr4i 
 |-  ( B ( R |` A ) C <-> B ( R i^i ( A X. ran ( R |` A ) ) ) C )