bj-iminvval2

Description: Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024)

	Ref	Expression
Hypotheses	bj-iminvval2.exa	$⊢ φ \to A \in U$
	bj-iminvval2.exb	$⊢ φ \to B \in V$
	bj-iminvval2.arg	$⊢ φ \to R \subseteq A \times B$
Assertion	bj-iminvval2	$⊢ φ \to (A 𝒫^{*} B) (R) = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land x = R^{-1} [y])\}$

Step	Hyp	Ref	Expression
1		bj-iminvval2.exa	$⊢ φ \to A \in U$
2		bj-iminvval2.exb	$⊢ φ \to B \in V$
3		bj-iminvval2.arg	$⊢ φ \to R \subseteq A \times B$
4	1 2	bj-iminvval	$⊢ φ \to A 𝒫^{*} B = (r \in 𝒫 (A \times B) ⟼ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land x = r^{-1} [y])\})$
5		simpr	$⊢ (φ \land r = R) \to r = R$
6	5	cnveqd	$⊢ (φ \land r = R) \to r^{-1} = R^{-1}$
7	6	imaeq1d	$⊢ (φ \land r = R) \to r^{-1} [y] = R^{-1} [y]$
8	7	eqeq2d	$⊢ (φ \land r = R) \to (x = r^{-1} [y] \leftrightarrow x = R^{-1} [y])$
9	8	anbi2d	$⊢ (φ \land r = R) \to (((x \subseteq A \land y \subseteq B) \land x = r^{-1} [y]) \leftrightarrow ((x \subseteq A \land y \subseteq B) \land x = R^{-1} [y]))$
10	9	opabbidv	$⊢ (φ \land r = R) \to \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land x = r^{-1} [y])\} = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land x = R^{-1} [y])\}$
11	1 2	xpexd	$⊢ φ \to A \times B \in V$
12	11 3	sselpwd	$⊢ φ \to R \in 𝒫 (A \times B)$
13	1 2	bj-imdirval2lem	$⊢ φ \to \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land x = R^{-1} [y])\} \in V$
14	4 10 12 13	fvmptd	$⊢ φ \to (A 𝒫^{*} B) (R) = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land x = R^{-1} [y])\}$

Metamath Proof Explorer