Metamath Proof Explorer

Theorem iinfprg

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

Ref Expression
Assertion iinfprg 
|- ( ( A e. V /\ B e. W ) -> ( x e. ( dom A i^i dom B ) |-> ( ( A ` x ) i^i ( B ` x ) ) ) = ( x e. |^|_ y e. { A , B } dom y |-> |^|_ y e. { A , B } ( y ` x ) ) )

Proof

Step Hyp Ref Expression
1 dmeq 
 |-  ( y = A -> dom y = dom A )
2 dmeq 
 |-  ( y = B -> dom y = dom B )
3 1 2 iinxprg 
 |-  ( ( A e. V /\ B e. W ) -> |^|_ y e. { A , B } dom y = ( dom A i^i dom B ) )
4 fveq1 
 |-  ( y = A -> ( y ` x ) = ( A ` x ) )
5 fveq1 
 |-  ( y = B -> ( y ` x ) = ( B ` x ) )
6 4 5 iinxprg 
 |-  ( ( A e. V /\ B e. W ) -> |^|_ y e. { A , B } ( y ` x ) = ( ( A ` x ) i^i ( B ` x ) ) )
7 3 6 mpteq12dv 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. |^|_ y e. { A , B } dom y |-> |^|_ y e. { A , B } ( y ` x ) ) = ( x e. ( dom A i^i dom B ) |-> ( ( A ` x ) i^i ( B ` x ) ) ) )
8 7 eqcomd 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. ( dom A i^i dom B ) |-> ( ( A ` x ) i^i ( B ` x ) ) ) = ( x e. |^|_ y e. { A , B } dom y |-> |^|_ y e. { A , B } ( y ` x ) ) )