Proof of Theorem mptmpt2opabbrd
Step | Hyp | Ref
| Expression |
1 | | mptmpt2opabbrd.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝑊) |
2 | | mptmpt2opabbrd.m |
. . . . . 6
⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)})) |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊) → 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}))) |
4 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝐴‘𝑔) = (𝐴‘𝐺)) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝐵‘𝑔) = (𝐵‘𝐺)) |
6 | | mptmpt2opabbrd.2 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏)) |
7 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝐷‘𝑔) = (𝐷‘𝐺)) |
8 | 7 | breqd 4594 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑓(𝐷‘𝑔)ℎ ↔ 𝑓(𝐷‘𝐺)ℎ)) |
9 | 6, 8 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ) ↔ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ))) |
10 | 9 | opabbidv 4648 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
11 | 4, 5, 10 | mpt2eq123dv 6615 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) |
12 | 11 | adantl 481 |
. . . . 5
⊢ (((𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊) ∧ 𝑔 = 𝐺) → (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) |
13 | | elex 3185 |
. . . . . 6
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) |
14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊) → 𝐺 ∈ V) |
15 | | fvex 6113 |
. . . . . . 7
⊢ (𝐴‘𝐺) ∈ V |
16 | | fvex 6113 |
. . . . . . 7
⊢ (𝐵‘𝐺) ∈ V |
17 | 15, 16 | pm3.2i 470 |
. . . . . 6
⊢ ((𝐴‘𝐺) ∈ V ∧ (𝐵‘𝐺) ∈ V) |
18 | | mpt2exga 7135 |
. . . . . 6
⊢ (((𝐴‘𝐺) ∈ V ∧ (𝐵‘𝐺) ∈ V) → (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V) |
19 | 17, 18 | mp1i 13 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊) → (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) ∈ V) |
20 | 3, 12, 14, 19 | fvmptd 6197 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊) → (𝑀‘𝐺) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) |
21 | 1, 1, 20 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑀‘𝐺) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})) |
22 | 21 | oveqd 6566 |
. 2
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌)) |
23 | | mptmpt2opabbrd.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) |
24 | | mptmpt2opabbrd.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) |
25 | | ancom 465 |
. . . . 5
⊢ ((𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)) |
26 | 25 | opabbii 4649 |
. . . 4
⊢
{〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} |
27 | | mptmpt2opabbrd.r |
. . . . 5
⊢ ((𝜑 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝜓) |
28 | | mptmpt2opabbrd.v |
. . . . 5
⊢ (𝜑 → {〈𝑓, ℎ〉 ∣ 𝜓} ∈ 𝑉) |
29 | 27, 28 | opabresex2d 40334 |
. . . 4
⊢ (𝜑 → {〈𝑓, ℎ〉 ∣ (𝑓(𝐷‘𝐺)ℎ ∧ 𝜃)} ∈ V) |
30 | 26, 29 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ V) |
31 | | mptmpt2opabbrd.1 |
. . . . . 6
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃)) |
32 | 31 | anbi1d 737 |
. . . . 5
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → ((𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ) ↔ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ))) |
33 | 32 | opabbidv 4648 |
. . . 4
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)} = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
34 | | eqid 2610 |
. . . 4
⊢ (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) = (𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
35 | 33, 34 | ovmpt2ga 6688 |
. . 3
⊢ ((𝑋 ∈ (𝐴‘𝐺) ∧ 𝑌 ∈ (𝐵‘𝐺) ∧ {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)} ∈ V) → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
36 | 23, 24, 30, 35 | syl3anc 1318 |
. 2
⊢ (𝜑 → (𝑋(𝑎 ∈ (𝐴‘𝐺), 𝑏 ∈ (𝐵‘𝐺) ↦ {〈𝑓, ℎ〉 ∣ (𝜏 ∧ 𝑓(𝐷‘𝐺)ℎ)})𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |
37 | 22, 36 | eqtrd 2644 |
1
⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) |