bj-imdirval2

Description: Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023)

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

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

Metamath Proof Explorer