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	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
	brcnvrabga.2	$$⊢R={\left\{⟨⟨y,z⟩,x⟩|\phi \right\}}^{-1}$$
Assertion	brcnvrabga	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(AR⟨B,C⟩\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		brrabga.1	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		brcnvrabga.2	$$⊢R={\left\{⟨⟨y,z⟩,x⟩|\phi \right\}}^{-1}$$
3		relcnv	$$⊢\mathrm{Rel}{\left\{⟨⟨y,z⟩,x⟩|\phi \right\}}^{-1}$$
4	2	releqi	$$⊢\mathrm{Rel}R\leftrightarrow \mathrm{Rel}{\left\{⟨⟨y,z⟩,x⟩|\phi \right\}}^{-1}$$
5	3 4	mpbir	$$⊢\mathrm{Rel}R$$
6	5	relbrcnv	$$⊢⟨B,C⟩R^{-1}A\leftrightarrow AR⟨B,C⟩$$
7	1	3coml	$$⊢\left(y=B\wedge z=C\wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
8	2	cnveqi	$$⊢R^{-1}={{\left\{⟨⟨y,z⟩,x⟩|\phi \right\}}^{-1}}^{-1}$$
9		reloprab	$$⊢\mathrm{Rel}\left\{⟨⟨y,z⟩,x⟩|\phi \right\}$$
10		dfrel2	$$⊢\mathrm{Rel}\left\{⟨⟨y,z⟩,x⟩|\phi \right\}\leftrightarrow {{\left\{⟨⟨y,z⟩,x⟩|\phi \right\}}^{-1}}^{-1}=\left\{⟨⟨y,z⟩,x⟩|\phi \right\}$$
11	9 10	mpbi	$$⊢{{\left\{⟨⟨y,z⟩,x⟩|\phi \right\}}^{-1}}^{-1}=\left\{⟨⟨y,z⟩,x⟩|\phi \right\}$$
12	8 11	eqtri	$$⊢R^{-1}=\left\{⟨⟨y,z⟩,x⟩|\phi \right\}$$
13	7 12	brrabga	$$⊢\left(B\in W\wedge C\in X\wedge A\in V\right)\to \left(⟨B,C⟩R^{-1}A\leftrightarrow \psi \right)$$
14	13	3comr	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(⟨B,C⟩R^{-1}A\leftrightarrow \psi \right)$$
15	6 14	bitr3id	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(AR⟨B,C⟩\leftrightarrow \psi \right)$$