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 ) )