Theorem bj-iminvval

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

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

Proof

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