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 ⊢ φ → G ∈ W
mptmpoopabbrdOLD.x ⊢ φ → X ∈ A ⁡ G
mptmpoopabbrdOLD.y ⊢ φ → Y ∈ B ⁡ G
mptmpoopabbrdOLD.v ⊢ φ → f h | ψ ∈ V
mptmpoopabbrdOLD.r ⊢ φ ∧ f D ⁡ G h → ψ
mptmpoopabovdOLD.m ⊢ M = g ∈ V ⟼ a ∈ A ⁡ g , b ∈ B ⁡ g ⟼ f h | f a C ⁡ g b h ∧ f D ⁡ g h
Assertion mptmpoopabovdOLD ⊢ φ → X M ⁡ G Y = f h | f X C ⁡ G Y h ∧ f D ⁡ G h

Proof

Step Hyp Ref Expression
1 mptmpoopabbrdOLD.g ⊢ φ → G ∈ W
2 mptmpoopabbrdOLD.x ⊢ φ → X ∈ A ⁡ G
3 mptmpoopabbrdOLD.y ⊢ φ → Y ∈ B ⁡ G
4 mptmpoopabbrdOLD.v ⊢ φ → f h | ψ ∈ V
5 mptmpoopabbrdOLD.r ⊢ φ ∧ f D ⁡ G h → ψ
6 mptmpoopabovdOLD.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 mptmpoopabbrdOLDOLD ⊢ φ → X M ⁡ G Y = f h | f X C ⁡ G Y h ∧ f D ⁡ G h