Proof of Theorem mptmpoopabbrd
| 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 | | fvex 6919 |
. . . . . . 7
⊢ (𝐷‘𝐺) ∈ V |
| 15 | 14 | pwex 5380 |
. . . . . 6
⊢ 𝒫
(𝐷‘𝐺) ∈ V |
| 16 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝑓(𝐷‘𝐺)ℎ) |
| 17 | 16 | ssopab2i 5555 |
. . . . . . . . 9
⊢
{〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ⊆ {〈𝑓, ℎ〉 ∣ 𝑓(𝐷‘𝐺)ℎ} |
| 18 | | opabss 5207 |
. . . . . . . . 9
⊢
{〈𝑓, ℎ〉 ∣ 𝑓(𝐷‘𝐺)ℎ} ⊆ (𝐷‘𝐺) |
| 19 | 17, 18 | sstri 3993 |
. . . . . . . 8
⊢
{〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ⊆ (𝐷‘𝐺) |
| 20 | 14, 19 | elpwi2 5335 |
. . . . . . 7
⊢
{〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ 𝒫 (𝐷‘𝐺) |
| 21 | 20 | rgen2w 3066 |
. . . . . 6
⊢
∀𝑎 ∈
(𝐴‘𝐺)∀𝑏 ∈ (𝐵‘𝐺){〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ 𝒫 (𝐷‘𝐺) |
| 22 | 12, 13, 15, 21 | mpoexw 8103 |
. . . . 5
⊢ (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V |
| 23 | 22 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V) |
| 24 | 1, 9, 11, 23 | fvmptd3 7039 |
. . 3
⊢ (𝜑 → (𝑀‘𝐺) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) |
| 25 | 24 | oveqd 7448 |
. 2
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌)) |
| 26 | | mptmpoopabbrd.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) |
| 27 | | mptmpoopabbrd.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) |
| 28 | | mptmpoopabbrd.1 |
. . . . . 6
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃)) |
| 29 | 28 | anbi1d 631 |
. . . . 5
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → ((𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ))) |
| 30 | 29 | opabbidv 5209 |
. . . 4
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
| 31 | | eqid 2737 |
. . . 4
⊢ (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
| 32 | | ancom 460 |
. . . . . 6
⊢ ((𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)) |
| 33 | 32 | opabbii 5210 |
. . . . 5
⊢
{〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} |
| 34 | | opabresex2 7485 |
. . . . 5
⊢
{〈𝑓, ℎ〉 ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} ∈ V |
| 35 | 33, 34 | eqeltri 2837 |
. . . 4
⊢
{〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ V |
| 36 | 30, 31, 35 | ovmpoa 7588 |
. . 3
⊢ ((𝑋 ∈ (𝐴‘𝐺) ∧ 𝑌 ∈ (𝐵‘𝐺)) → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
| 37 | 26, 27, 36 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
| 38 | 25, 37 | eqtrd 2777 |
1
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |