Theorem bj-imdirval

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

	Ref	Expression
Hypotheses	bj-imdirval.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	bj-imdirval.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
Assertion	bj-imdirval	⊢ ( 𝜑 → ( 𝐴 𝒫* 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		bj-imdirval.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		df-imdir	⊢ 𝒫* = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } ) )
4	1 2 3	bj-imdirvallem	⊢ ( 𝜑 → ( 𝐴 𝒫* 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } ) )