Theorem fsovfvd

Description: Value of the operator, ( A O B ) , which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, A and B , when applied to function F . (Contributed by RP, 25-Apr-2021)

	Ref	Expression
Hypotheses	fsovd.fs	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
	fsovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fsovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	fsovfvd.g	⊢ 𝐺 = ( 𝐴 𝑂 𝐵 )
	fsovfvd.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) )
Assertion	fsovfvd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		fsovd.fs	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
2		fsovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		fsovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		fsovfvd.g	⊢ 𝐺 = ( 𝐴 𝑂 𝐵 )
5		fsovfvd.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) )
6	1 2 3	fsovd	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
7	4 6	syl5eq	⊢ ( 𝜑 → 𝐺 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
8		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9	8	eleq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
10	9	rabbidv	⊢ ( 𝑓 = 𝐹 → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } )
11	10	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) )
13	3	mptexd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) ∈ V )
14	7 12 5 13	fvmptd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) )