Step | Hyp | Ref
| Expression |
1 | | mptmpoopabbrd.m |
. . . 4
⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)})) |
2 | | fveq2 6891 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝐴‘𝑔) = (𝐴‘𝐺)) |
3 | | fveq2 6891 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝐵‘𝑔) = (𝐵‘𝐺)) |
4 | | mptmpoopabbrd.2 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏)) |
5 | | fveq2 6891 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝐷‘𝑔) = (𝐷‘𝐺)) |
6 | 5 | breqd 5153 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑓(𝐷‘𝑔)ℎ ↔ 𝑓(𝐷‘𝐺)ℎ)) |
7 | 4, 6 | anbi12d 630 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ) ↔ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ))) |
8 | 7 | opabbidv 5208 |
. . . . 5
⊢ (𝑔 = 𝐺 → {⟨𝑓, ℎ⟩ ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)} = {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
9 | 2, 3, 8 | mpoeq123dv 7489 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) |
10 | | mptmpoopabbrd.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑊) |
11 | 10 | elexd 3490 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ V) |
12 | | fvex 6904 |
. . . . . 6
⊢ (𝐴‘𝐺) ∈ V |
13 | | fvex 6904 |
. . . . . 6
⊢ (𝐵‘𝐺) ∈ V |
14 | | fvex 6904 |
. . . . . . 7
⊢ (𝐷‘𝐺) ∈ V |
15 | 14 | pwex 5374 |
. . . . . 6
⊢ 𝒫
(𝐷‘𝐺) ∈ V |
16 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝑓(𝐷‘𝐺)ℎ) |
17 | 16 | ssopab2i 5546 |
. . . . . . . . 9
⊢
{⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ⊆ {⟨𝑓, ℎ⟩ ∣ 𝑓(𝐷‘𝐺)ℎ} |
18 | | opabss 5206 |
. . . . . . . . 9
⊢
{⟨𝑓, ℎ⟩ ∣ 𝑓(𝐷‘𝐺)ℎ} ⊆ (𝐷‘𝐺) |
19 | 17, 18 | sstri 3987 |
. . . . . . . 8
⊢
{⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ⊆ (𝐷‘𝐺) |
20 | 14, 19 | elpwi2 5342 |
. . . . . . 7
⊢
{⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ 𝒫 (𝐷‘𝐺) |
21 | 20 | rgen2w 3061 |
. . . . . 6
⊢
∀𝑎 ∈
(𝐴‘𝐺)∀𝑏 ∈ (𝐵‘𝐺){⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ 𝒫 (𝐷‘𝐺) |
22 | 12, 13, 15, 21 | mpoexw 8077 |
. . . . 5
⊢ (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V |
23 | 22 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V) |
24 | 1, 9, 11, 23 | fvmptd3 7022 |
. . 3
⊢ (𝜑 → (𝑀‘𝐺) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) |
25 | 24 | oveqd 7431 |
. 2
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌)) |
26 | | mptmpoopabbrd.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) |
27 | | mptmpoopabbrd.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) |
28 | | mptmpoopabbrd.1 |
. . . . . 6
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃)) |
29 | 28 | anbi1d 629 |
. . . . 5
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → ((𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ))) |
30 | 29 | opabbidv 5208 |
. . . 4
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
31 | | eqid 2727 |
. . . 4
⊢ (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
32 | | ancom 460 |
. . . . . 6
⊢ ((𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)) |
33 | 32 | opabbii 5209 |
. . . . 5
⊢
{⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {⟨𝑓, ℎ⟩ ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} |
34 | | opabresex2 7466 |
. . . . 5
⊢
{⟨𝑓, ℎ⟩ ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} ∈ V |
35 | 33, 34 | eqeltri 2824 |
. . . 4
⊢
{⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ V |
36 | 30, 31, 35 | ovmpoa 7570 |
. . 3
⊢ ((𝑋 ∈ (𝐴‘𝐺) ∧ 𝑌 ∈ (𝐵‘𝐺)) → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
37 | 26, 27, 36 | syl2anc 583 |
. 2
⊢ (𝜑 → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
38 | 25, 37 | eqtrd 2767 |
1
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |