Theorem iinfprg

Description: Indexed intersection of functions with an unordered pair index. (Contributed by Zhi Wang, 31-Oct-2025)

	Ref	Expression
Assertion	iinfprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑥 ) ∩ ( 𝐵 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } dom 𝑦 ↦ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑦 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmeq	⊢ ( 𝑦 = 𝐴 → dom 𝑦 = dom 𝐴 )
2		dmeq	⊢ ( 𝑦 = 𝐵 → dom 𝑦 = dom 𝐵 )
3	1 2	iinxprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ 𝑦 ∈ { 𝐴 , 𝐵 } dom 𝑦 = ( dom 𝐴 ∩ dom 𝐵 ) )
4		fveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
5		fveq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
6	4 5	iinxprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑦 ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ∩ ( 𝐵 ‘ 𝑥 ) ) )
7	3 6	mpteq12dv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } dom 𝑦 ↦ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑦 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑥 ) ∩ ( 𝐵 ‘ 𝑥 ) ) ) )
8	7	eqcomd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑥 ) ∩ ( 𝐵 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } dom 𝑦 ↦ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑦 ‘ 𝑥 ) ) )