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

Metamath Proof Explorer

Theorem brcnvrabga

Description: The law of concretion for the converse of operation class abstraction. (Contributed by Peter Mazsa, 25-Oct-2022)

Ref Expression
Hypotheses brrabga.1 
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
brcnvrabga.2 
|- R = `' { <. <. y , z >. , x >. | ph }
Assertion brcnvrabga 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A R <. B , C >. <-> ps ) )

Proof

Step Hyp Ref Expression
1 brrabga.1 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
2 brcnvrabga.2 
 |-  R = `' { <. <. y , z >. , x >. | ph }
3 relcnv 
 |-  Rel `' { <. <. y , z >. , x >. | ph }
4 2 releqi 
 |-  ( Rel R <-> Rel `' { <. <. y , z >. , x >. | ph } )
5 3 4 mpbir 
 |-  Rel R
6 5 relbrcnv 
 |-  ( <. B , C >. `' R A <-> A R <. B , C >. )
7 1 3coml 
 |-  ( ( y = B /\ z = C /\ x = A ) -> ( ph <-> ps ) )
8 2 cnveqi 
 |-  `' R = `' `' { <. <. y , z >. , x >. | ph }
9 reloprab 
 |-  Rel { <. <. y , z >. , x >. | ph }
10 dfrel2 
 |-  ( Rel { <. <. y , z >. , x >. | ph } <-> `' `' { <. <. y , z >. , x >. | ph } = { <. <. y , z >. , x >. | ph } )
11 9 10 mpbi 
 |-  `' `' { <. <. y , z >. , x >. | ph } = { <. <. y , z >. , x >. | ph }
12 8 11 eqtri 
 |-  `' R = { <. <. y , z >. , x >. | ph }
13 7 12 brrabga 
 |-  ( ( B e. W /\ C e. X /\ A e. V ) -> ( <. B , C >. `' R A <-> ps ) )
14 13 3comr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. B , C >. `' R A <-> ps ) )
15 6 14 bitr3id 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A R <. B , C >. <-> ps ) )