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 ∈ V ∧ B ∈ W → x ∈ dom ⁡ A ∩ dom ⁡ B ⟼ A ⁡ x ∩ B ⁡ x = x ∈ ⋂ y ∈ A B dom ⁡ y ⟼ ⋂ y ∈ 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 ∈ V ∧ B ∈ W → ⋂ y ∈ A B dom ⁡ y = dom ⁡ A ∩ dom ⁡ B
4 fveq1 ⊢ y = A → y ⁡ x = A ⁡ x
5 fveq1 ⊢ y = B → y ⁡ x = B ⁡ x
6 4 5 iinxprg ⊢ A ∈ V ∧ B ∈ W → ⋂ y ∈ A B y ⁡ x = A ⁡ x ∩ B ⁡ x
7 3 6 mpteq12dv ⊢ A ∈ V ∧ B ∈ W → x ∈ ⋂ y ∈ A B dom ⁡ y ⟼ ⋂ y ∈ A B y ⁡ x = x ∈ dom ⁡ A ∩ dom ⁡ B ⟼ A ⁡ x ∩ B ⁡ x
8 7 eqcomd ⊢ A ∈ V ∧ B ∈ W → x ∈ dom ⁡ A ∩ dom ⁡ B ⟼ A ⁡ x ∩ B ⁡ x = x ∈ ⋂ y ∈ A B dom ⁡ y ⟼ ⋂ y ∈ A B y ⁡ x