Theorem fsovfd

Description: 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 , gives a function between two sets of functions. (Contributed by RP, 27-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		fsovd.fs	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
2		fsovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		fsovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		fsovfvd.g	⊢ 𝐺 = ( 𝐴 𝑂 𝐵 )
5	1 2 3	fsovd	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
6	4 5	eqtrid	⊢ ( 𝜑 → 𝐺 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
7		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ⊆ 𝐴
8	7	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ⊆ 𝐴 )
9	2 8	sselpwd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ 𝒫 𝐴 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ 𝒫 𝐴 )
11	10	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) : 𝐵 ⟶ 𝒫 𝐴 )
12	2	pwexd	⊢ ( 𝜑 → 𝒫 𝐴 ∈ V )
13	12 3	elmapd	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) : 𝐵 ⟶ 𝒫 𝐴 ) )
14	11 13	mpbird	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ∈ ( 𝒫 𝐴 ↑m 𝐵 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ∈ ( 𝒫 𝐴 ↑m 𝐵 ) )
16	6 15	fmpt3d	⊢ ( 𝜑 → 𝐺 : ( 𝒫 𝐵 ↑m 𝐴 ) ⟶ ( 𝒫 𝐴 ↑m 𝐵 ) )