Theorem bj-imdirval2

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

	Ref	Expression
Hypotheses	bj-imdirval2.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	bj-imdirval2.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	bj-imdirval2.arg	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝐴 × 𝐵 ) )
Assertion	bj-imdirval2	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐵 ) ‘ 𝑅 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval2.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		bj-imdirval2.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		bj-imdirval2.arg	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝐴 × 𝐵 ) )
4	1 2	bj-imdirval	⊢ ( 𝜑 → ( 𝐴 𝒫* 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } ) )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
6	5	imaeq1d	⊢ ( ( 𝜑 ∧ 𝑟 = 𝑅 ) → ( 𝑟 “ 𝑥 ) = ( 𝑅 “ 𝑥 ) )
7	6	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑟 = 𝑅 ) → ( ( 𝑟 “ 𝑥 ) = 𝑦 ↔ ( 𝑅 “ 𝑥 ) = 𝑦 ) )
8	7	anbi2d	⊢ ( ( 𝜑 ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
9	8	opabbidv	⊢ ( ( 𝜑 ∧ 𝑟 = 𝑅 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } )
10	1 2	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
11	10 3	sselpwd	⊢ ( 𝜑 → 𝑅 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
12	1 2	bj-imdirval2lem	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } ∈ V )
13	4 9 11 12	fvmptd	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐵 ) ‘ 𝑅 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } )