Step | Hyp | Ref
| Expression |
1 | | df-br 5107 |
. . 3
β’ (πΉ β€ πΊ β β¨πΉ, πΊβ© β β€ ) |
2 | | prdsbasmpt.y |
. . . . . 6
β’ π = (πXsπ
) |
3 | | prdsbasmpt.s |
. . . . . 6
β’ (π β π β π) |
4 | | prdsbasmpt.r |
. . . . . . 7
β’ (π β π
Fn πΌ) |
5 | | prdsbasmpt.i |
. . . . . . 7
β’ (π β πΌ β π) |
6 | | fnex 7168 |
. . . . . . 7
β’ ((π
Fn πΌ β§ πΌ β π) β π
β V) |
7 | 4, 5, 6 | syl2anc 585 |
. . . . . 6
β’ (π β π
β V) |
8 | | prdsbasmpt.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
9 | 4 | fndmd 6608 |
. . . . . 6
β’ (π β dom π
= πΌ) |
10 | | prdsleval.l |
. . . . . 6
β’ β€ =
(leβπ) |
11 | 2, 3, 7, 8, 9, 10 | prdsle 17349 |
. . . . 5
β’ (π β β€ = {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}) |
12 | | vex 3448 |
. . . . . . . 8
β’ π β V |
13 | | vex 3448 |
. . . . . . . 8
β’ π β V |
14 | 12, 13 | prss 4781 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β {π, π} β π΅) |
15 | 14 | anbi1i 625 |
. . . . . 6
β’ (((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯)) β ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))) |
16 | 15 | opabbii 5173 |
. . . . 5
β’
{β¨π, πβ© β£ ((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))} = {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))} |
17 | 11, 16 | eqtr4di 2791 |
. . . 4
β’ (π β β€ = {β¨π, πβ© β£ ((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}) |
18 | 17 | eleq2d 2820 |
. . 3
β’ (π β (β¨πΉ, πΊβ© β β€ β β¨πΉ, πΊβ© β {β¨π, πβ© β£ ((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))})) |
19 | 1, 18 | bitrid 283 |
. 2
β’ (π β (πΉ β€ πΊ β β¨πΉ, πΊβ© β {β¨π, πβ© β£ ((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))})) |
20 | | prdsplusgval.f |
. . 3
β’ (π β πΉ β π΅) |
21 | | prdsplusgval.g |
. . 3
β’ (π β πΊ β π΅) |
22 | | fveq1 6842 |
. . . . . 6
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
23 | | fveq1 6842 |
. . . . . 6
β’ (π = πΊ β (πβπ₯) = (πΊβπ₯)) |
24 | 22, 23 | breqan12d 5122 |
. . . . 5
β’ ((π = πΉ β§ π = πΊ) β ((πβπ₯)(leβ(π
βπ₯))(πβπ₯) β (πΉβπ₯)(leβ(π
βπ₯))(πΊβπ₯))) |
25 | 24 | ralbidv 3171 |
. . . 4
β’ ((π = πΉ β§ π = πΊ) β (βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯) β βπ₯ β πΌ (πΉβπ₯)(leβ(π
βπ₯))(πΊβπ₯))) |
26 | 25 | opelopab2a 5493 |
. . 3
β’ ((πΉ β π΅ β§ πΊ β π΅) β (β¨πΉ, πΊβ© β {β¨π, πβ© β£ ((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))} β βπ₯ β πΌ (πΉβπ₯)(leβ(π
βπ₯))(πΊβπ₯))) |
27 | 20, 21, 26 | syl2anc 585 |
. 2
β’ (π β (β¨πΉ, πΊβ© β {β¨π, πβ© β£ ((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))} β βπ₯ β πΌ (πΉβπ₯)(leβ(π
βπ₯))(πΊβπ₯))) |
28 | 19, 27 | bitrd 279 |
1
β’ (π β (πΉ β€ πΊ β βπ₯ β πΌ (πΉβπ₯)(leβ(π
βπ₯))(πΊβπ₯))) |