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)

Ref Expression
Hypotheses mptmpoopabbrd.g ⊢ φ → G ∈ W
mptmpoopabbrd.x ⊢ φ → X ∈ A ⁡ G
mptmpoopabbrd.y ⊢ φ → Y ∈ B ⁡ G
mptmpoopabbrd.v ⊢ φ → f h | ψ ∈ V
mptmpoopabbrd.r ⊢ φ ∧ f D ⁡ G h → ψ
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 mptmpoopabbrd.v ⊢ φ → f h | ψ ∈ V
5 mptmpoopabbrd.r ⊢ φ ∧ f D ⁡ G h → ψ
6 mptmpoopabovd.m ⊢ M = g ∈ V ⟼ a ∈ A ⁡ g , b ∈ B ⁡ g ⟼ f h | f a C ⁡ g b h ∧ f D ⁡ g h
7 oveq12 ⊢ a = X ∧ b = Y → a C ⁡ G b = X C ⁡ G Y
8 7 breqd ⊢ a = X ∧ b = Y → f a C ⁡ G b h ↔ f X C ⁡ G Y h
9 fveq2 ⊢ g = G → C ⁡ g = C ⁡ G
10 9 oveqd ⊢ g = G → a C ⁡ g b = a C ⁡ G b
11 10 breqd ⊢ g = G → f a C ⁡ g b h ↔ f a C ⁡ G b h
12 1 2 3 4 5 8 11 6 mptmpoopabbrd ⊢ φ → X M ⁡ G Y = f h | f X C ⁡ G Y h ∧ f D ⁡ G h