Metamath Proof Explorer

Theorem mptmpoopabovd

Description: The operation value of a function value of a collection of ordered pairs of related elements. (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) Add disjoint variable condition on D , f , h to remove hypotheses. (Revised by SN, 13-Dec-2024)

Ref Expression
Hypotheses mptmpoopabbrd.g ⊢ φ → G ∈ W
mptmpoopabbrd.x ⊢ φ → X ∈ A ⁡ G
mptmpoopabbrd.y ⊢ φ → Y ∈ B ⁡ G
mptmpoopabovd.m ⊢ M = g ∈ V ⟼ a ∈ A ⁡ g , b ∈ B ⁡ g ⟼ f h | f a C ⁡ g b h ∧ f D ⁡ g h
Assertion mptmpoopabovd ⊢ φ → X M ⁡ G Y = f h | f X C ⁡ G Y h ∧ f D ⁡ G h

Proof

Step Hyp Ref Expression
1 mptmpoopabbrd.g ⊢ φ → G ∈ W
2 mptmpoopabbrd.x ⊢ φ → X ∈ A ⁡ G
3 mptmpoopabbrd.y ⊢ φ → Y ∈ B ⁡ G
4 mptmpoopabovd.m ⊢ M = g ∈ V ⟼ a ∈ A ⁡ g , b ∈ B ⁡ g ⟼ f h | f a C ⁡ g b h ∧ f D ⁡ g h
5 oveq12 ⊢ a = X ∧ b = Y → a C ⁡ G b = X C ⁡ G Y
6 5 breqd ⊢ a = X ∧ b = Y → f a C ⁡ G b h ↔ f X C ⁡ G Y h
7 fveq2 ⊢ g = G → C ⁡ g = C ⁡ G
8 7 oveqd ⊢ g = G → a C ⁡ g b = a C ⁡ G b
9 8 breqd ⊢ g = G → f a C ⁡ g b h ↔ f a C ⁡ G b h
10 1 2 3 6 9 4 mptmpoopabbrd ⊢ φ → X M ⁡ G Y = f h | f X C ⁡ G Y h ∧ f D ⁡ G h