Theorem mptmpoopabbrd

Description: The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) Add disjoint variable condition on D , f , h to remove hypotheses; avoid ax-rep . (Revised by SN, 7-Apr-2025)

	Ref	Expression
Hypotheses	mptmpoopabbrd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	mptmpoopabbrd.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) )
	mptmpoopabbrd.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) )
	mptmpoopabbrd.1	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( 𝜏 ↔ 𝜃 ) )
	mptmpoopabbrd.2	⊢ ( 𝑔 = 𝐺 → ( 𝜒 ↔ 𝜏 ) )
	mptmpoopabbrd.m	⊢ 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) )
Assertion	mptmpoopabbrd	⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )

Proof

Step	Hyp	Ref	Expression
1		mptmpoopabbrd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
2		mptmpoopabbrd.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) )
3		mptmpoopabbrd.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) )
4		mptmpoopabbrd.1	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( 𝜏 ↔ 𝜃 ) )
5		mptmpoopabbrd.2	⊢ ( 𝑔 = 𝐺 → ( 𝜒 ↔ 𝜏 ) )
6		mptmpoopabbrd.m	⊢ 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) )
7		fveq2	⊢ ( 𝑔 = 𝐺 → ( 𝐴 ‘ 𝑔 ) = ( 𝐴 ‘ 𝐺 ) )
8		fveq2	⊢ ( 𝑔 = 𝐺 → ( 𝐵 ‘ 𝑔 ) = ( 𝐵 ‘ 𝐺 ) )
9		fveq2	⊢ ( 𝑔 = 𝐺 → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝐺 ) )
10	9	breqd	⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ↔ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) )
11	5 10	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) ↔ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ) )
12	11	opabbidv	⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
13	7 8 12	mpoeq123dv	⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) )
14	1	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
15		fvex	⊢ ( 𝐴 ‘ 𝐺 ) ∈ V
16		fvex	⊢ ( 𝐵 ‘ 𝐺 ) ∈ V
17		fvex	⊢ ( 𝐷 ‘ 𝐺 ) ∈ V
18	17	pwex	⊢ 𝒫 ( 𝐷 ‘ 𝐺 ) ∈ V
19		simpr	⊢ ( ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) → 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ )
20	19	ssopab2i	⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ⊆ { ⟨ 𝑓 , ℎ ⟩ ∣ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ }
21		opabss	⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ } ⊆ ( 𝐷 ‘ 𝐺 )
22	20 21	sstri	⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ⊆ ( 𝐷 ‘ 𝐺 )
23	17 22	elpwi2	⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ∈ 𝒫 ( 𝐷 ‘ 𝐺 )
24	23	rgen2w	⊢ ∀ 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) ∀ 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ∈ 𝒫 ( 𝐷 ‘ 𝐺 )
25	15 16 18 24	mpoexw	⊢ ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) ∈ V
26	25	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) ∈ V )
27	6 13 14 26	fvmptd3	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐺 ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) )
28	27	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) )
29	4	anbi1d	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ↔ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ) )
30	29	opabbidv	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
31		eqid	⊢ ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
32		ancom	⊢ ( ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ↔ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) )
33	32	opabbii	⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) }
34		opabresex2	⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) } ∈ V
35	33 34	eqeltri	⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ∈ V
36	30 31 35	ovmpoa	⊢ ( ( 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) ∧ 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) ) → ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
37	2 3 36	syl2anc	⊢ ( 𝜑 → ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
38	28 37	eqtrd	⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )