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	$⊢ φ \to G \in W$
	mptmpoopabbrd.x	$⊢ φ \to X \in A (G)$
	mptmpoopabbrd.y	$⊢ φ \to Y \in B (G)$
	mptmpoopabovd.m	$⊢ M = (g \in V ⟼ (a \in A (g), b \in B (g) ⟼ \{⟨f, h⟩ \| (f (a C (g) b) h \land f D (g) h)\}))$
Assertion	mptmpoopabovd	$⊢ φ \to X M (G) Y = \{⟨f, h⟩ \| (f (X C (G) Y) h \land f D (G) h)\}$

Proof

Step	Hyp	Ref	Expression
1		mptmpoopabbrd.g	$⊢ φ \to G \in W$
2		mptmpoopabbrd.x	$⊢ φ \to X \in A (G)$
3		mptmpoopabbrd.y	$⊢ φ \to Y \in B (G)$
4		mptmpoopabovd.m	$⊢ M = (g \in V ⟼ (a \in A (g), b \in B (g) ⟼ \{⟨f, h⟩ \| (f (a C (g) b) h \land f D (g) h)\}))$
5		oveq12	$⊢ (a = X \land b = Y) \to a C (G) b = X C (G) Y$
6	5	breqd	$⊢ (a = X \land b = Y) \to (f (a C (G) b) h \leftrightarrow f (X C (G) Y) h)$
7		fveq2	$⊢ g = G \to C (g) = C (G)$
8	7	oveqd	$⊢ g = G \to a C (g) b = a C (G) b$
9	8	breqd	$⊢ g = G \to (f (a C (g) b) h \leftrightarrow f (a C (G) b) h)$
10	1 2 3 6 9 4	mptmpoopabbrd	$⊢ φ \to X M (G) Y = \{⟨f, h⟩ \| (f (X C (G) Y) h \land f D (G) h)\}$

Metamath Proof Explorer

Theorem mptmpoopabovd

Proof