Metamath Proof Explorer

Theorem mptmpoopabovdOLD

Description: Obsolete version of mptmpoopabovd as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	mptmpoopabbrdOLD.g	$⊢ φ \to G \in W$
		mptmpoopabbrdOLD.x	$⊢ φ \to X \in A (G)$
		mptmpoopabbrdOLD.y	$⊢ φ \to Y \in B (G)$
		mptmpoopabbrdOLD.v	$⊢ φ \to \{⟨f, h⟩ \| ψ\} \in V$
		mptmpoopabbrdOLD.r	$⊢ (φ \land f D (G) h) \to ψ$
		mptmpoopabovdOLD.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	mptmpoopabovdOLD	$⊢ φ \to X M (G) Y = \{⟨f, h⟩ \| (f (X C (G) Y) h \land f D (G) h)\}$

Proof

Step	Hyp	Ref	Expression
1		mptmpoopabbrdOLD.g	$⊢ φ \to G \in W$
2		mptmpoopabbrdOLD.x	$⊢ φ \to X \in A (G)$
3		mptmpoopabbrdOLD.y	$⊢ φ \to Y \in B (G)$
4		mptmpoopabbrdOLD.v	$⊢ φ \to \{⟨f, h⟩ \| ψ\} \in V$
5		mptmpoopabbrdOLD.r	$⊢ (φ \land f D (G) h) \to ψ$
6		mptmpoopabovdOLD.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)\}))$
7		oveq12	$⊢ (a = X \land b = Y) \to a C (G) b = X C (G) Y$
8	7	breqd	$⊢ (a = X \land b = Y) \to (f (a C (G) b) h \leftrightarrow f (X C (G) Y) h)$
9		fveq2	$⊢ g = G \to C (g) = C (G)$
10	9	oveqd	$⊢ g = G \to a C (g) b = a C (G) b$
11	10	breqd	$⊢ g = G \to (f (a C (g) b) h \leftrightarrow f (a C (G) b) h)$
12	1 2 3 4 5 8 11 6	mptmpoopabbrdOLDOLD	$⊢ φ \to X M (G) Y = \{⟨f, h⟩ \| (f (X C (G) Y) h \land f D (G) h)\}$