Metamath Proof Explorer

Theorem bj-imdirval

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

	Ref	Expression
Hypotheses	bj-imdirval.1	$⊢ φ \to A \in U$
	bj-imdirval.2	$⊢ φ \to B \in V$
Assertion	bj-imdirval	$⊢ φ \to A 𝒫_{*} B = (r \in 𝒫 (A \times B) ⟼ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land r [x] = y)\})$

Step	Hyp	Ref	Expression
1		bj-imdirval.1	$⊢ φ \to A \in U$
2		bj-imdirval.2	$⊢ φ \to B \in V$
3		df-imdir	$⊢ 𝒫_{*} = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land r [x] = y)\}))$
4	1 2 3	bj-imdirvallem	$⊢ φ \to A 𝒫_{*} B = (r \in 𝒫 (A \times B) ⟼ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land r [x] = y)\})$