Theorem bj-iminvval2

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

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

Proof

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