Proof of Theorem mptmpoopabbrdOLD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mptmpoopabbrd.m | . . . 4
⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)})) | 
| 2 |  | fveq2 6906 | . . . . 5
⊢ (𝑔 = 𝐺 → (𝐴‘𝑔) = (𝐴‘𝐺)) | 
| 3 |  | fveq2 6906 | . . . . 5
⊢ (𝑔 = 𝐺 → (𝐵‘𝑔) = (𝐵‘𝐺)) | 
| 4 |  | mptmpoopabbrd.2 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏)) | 
| 5 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝐷‘𝑔) = (𝐷‘𝐺)) | 
| 6 | 5 | breqd 5154 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑓(𝐷‘𝑔)ℎ ↔ 𝑓(𝐷‘𝐺)ℎ)) | 
| 7 | 4, 6 | anbi12d 632 | . . . . . 6
⊢ (𝑔 = 𝐺 → ((𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ) ↔ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ))) | 
| 8 | 7 | opabbidv 5209 | . . . . 5
⊢ (𝑔 = 𝐺 → {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) | 
| 9 | 2, 3, 8 | mpoeq123dv 7508 | . . . 4
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) | 
| 10 |  | mptmpoopabbrd.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑊) | 
| 11 | 10 | elexd 3504 | . . . 4
⊢ (𝜑 → 𝐺 ∈ V) | 
| 12 |  | fvex 6919 | . . . . . 6
⊢ (𝐴‘𝐺) ∈ V | 
| 13 |  | fvex 6919 | . . . . . 6
⊢ (𝐵‘𝐺) ∈ V | 
| 14 | 12, 13 | mpoex 8104 | . . . . 5
⊢ (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V | 
| 15 | 14 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V) | 
| 16 | 1, 9, 11, 15 | fvmptd3 7039 | . . 3
⊢ (𝜑 → (𝑀‘𝐺) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) | 
| 17 | 16 | oveqd 7448 | . 2
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌)) | 
| 18 |  | mptmpoopabbrd.x | . . 3
⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) | 
| 19 |  | mptmpoopabbrd.y | . . 3
⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) | 
| 20 |  | mptmpoopabbrd.1 | . . . . . 6
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃)) | 
| 21 | 20 | anbi1d 631 | . . . . 5
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → ((𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ))) | 
| 22 | 21 | opabbidv 5209 | . . . 4
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) | 
| 23 |  | eqid 2737 | . . . 4
⊢ (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) | 
| 24 |  | ancom 460 | . . . . . 6
⊢ ((𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)) | 
| 25 | 24 | opabbii 5210 | . . . . 5
⊢
{〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} | 
| 26 |  | opabresex2 7485 | . . . . 5
⊢
{〈𝑓, ℎ〉 ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} ∈ V | 
| 27 | 25, 26 | eqeltri 2837 | . . . 4
⊢
{〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ V | 
| 28 | 22, 23, 27 | ovmpoa 7588 | . . 3
⊢ ((𝑋 ∈ (𝐴‘𝐺) ∧ 𝑌 ∈ (𝐵‘𝐺)) → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) | 
| 29 | 18, 19, 28 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) | 
| 30 | 17, 29 | eqtrd 2777 | 1
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |