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

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

Metamath Proof Explorer