Theorem fsovfvfvd

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 and element Y . (Contributed by RP, 25-Apr-2021)

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

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		fsovfvfvd.h	⊢ 𝐻 = ( 𝐺 ‘ 𝐹 )
7		fsovfvfvd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8	1 2 3 4 5	fsovfvd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) )
9	6 8	syl5eq	⊢ ( 𝜑 → 𝐻 = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) )
10		eleq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑌 ∈ ( 𝐹 ‘ 𝑥 ) ) )
11	10	rabbidv	⊢ ( 𝑦 = 𝑌 → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑌 ∈ ( 𝐹 ‘ 𝑥 ) } )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑌 ) → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑌 ∈ ( 𝐹 ‘ 𝑥 ) } )
13		rabexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝑌 ∈ ( 𝐹 ‘ 𝑥 ) } ∈ V )
14	2 13	syl	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝑌 ∈ ( 𝐹 ‘ 𝑥 ) } ∈ V )
15	9 12 7 14	fvmptd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑌 ) = { 𝑥 ∈ 𝐴 ∣ 𝑌 ∈ ( 𝐹 ‘ 𝑥 ) } )