Theorem rfovcnvfvd

Description: Value of the converse of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B , evaluated at function G . (Contributed by RP, 27-Apr-2021)

	Ref	Expression
Hypotheses	rfovd.rf	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) )
	rfovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	rfovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	rfovcnvf1od.f	⊢ 𝐹 = ( 𝐴 𝑂 𝐵 )
	rfovcnvfv.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) )
Assertion	rfovcnvfvd	⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝐺 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) )
2		rfovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		rfovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		rfovcnvf1od.f	⊢ 𝐹 = ( 𝐴 𝑂 𝐵 )
5		rfovcnvfv.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) )
6	1 2 3 4	rfovcnvd	⊢ ( 𝜑 → ◡ 𝐹 = ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) ) } ) )
7		fveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
8	7	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) ↔ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) )
9	8	anbi2d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) ) )
10	9	opabbidv	⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) } )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) } )
12		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝐴 )
13		elmapi	⊢ ( 𝐺 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → 𝐺 : 𝐴 ⟶ 𝒫 𝐵 )
14	13	ffvelrnda	⊢ ( ( 𝐺 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝒫 𝐵 )
15	5 14	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝒫 𝐵 )
16	15	elpwid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ⊆ 𝐵 )
17	16	sseld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) )
18	17	impr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑦 ∈ 𝐵 )
19	2 3 12 18	opabex2	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) } ∈ V )
20	6 11 5 19	fvmptd	⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝐺 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ) } )