Step | Hyp | Ref
| Expression |
1 | | mrsubffval.c |
. . . . . 6
β’ πΆ = (mCNβπ) |
2 | | mrsubffval.v |
. . . . . 6
β’ π = (mVRβπ) |
3 | | mrsubffval.r |
. . . . . 6
β’ π
= (mRExβπ) |
4 | | mrsubffval.s |
. . . . . 6
β’ π = (mRSubstβπ) |
5 | | mrsubffval.g |
. . . . . 6
β’ πΊ = (freeMndβ(πΆ βͺ π)) |
6 | 1, 2, 3, 4, 5 | mrsubffval 34165 |
. . . . 5
β’ (π β V β π = (π β (π
βpm π) β¦ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β π = (π β (π
βpm π) β¦ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |
8 | | dmeq 5863 |
. . . . . . . . . . 11
β’ (π = πΉ β dom π = dom πΉ) |
9 | | fdm 6681 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆπ
β dom πΉ = π΄) |
10 | 9 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β dom πΉ = π΄) |
11 | 8, 10 | sylan9eqr 2795 |
. . . . . . . . . 10
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β dom π = π΄) |
12 | 11 | eleq2d 2820 |
. . . . . . . . 9
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β (π£ β dom π β π£ β π΄)) |
13 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β π = πΉ) |
14 | 13 | fveq1d 6848 |
. . . . . . . . 9
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β (πβπ£) = (πΉβπ£)) |
15 | 12, 14 | ifbieq1d 4514 |
. . . . . . . 8
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β if(π£ β dom π, (πβπ£), β¨βπ£ββ©) = if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) |
16 | 15 | mpteq2dv 5211 |
. . . . . . 7
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β (π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) = (π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©))) |
17 | 16 | coeq1d 5821 |
. . . . . 6
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π) = ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π)) |
18 | 17 | oveq2d 7377 |
. . . . 5
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)) = (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))) |
19 | 18 | mpteq2dv 5211 |
. . . 4
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))) = (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π)))) |
20 | 3 | fvexi 6860 |
. . . . . 6
β’ π
β V |
21 | 20 | a1i 11 |
. . . . 5
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β π
β V) |
22 | 2 | fvexi 6860 |
. . . . . 6
β’ π β V |
23 | 22 | a1i 11 |
. . . . 5
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β π β V) |
24 | | simprl 770 |
. . . . 5
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β πΉ:π΄βΆπ
) |
25 | | simprr 772 |
. . . . 5
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β π΄ β π) |
26 | | elpm2r 8789 |
. . . . 5
β’ (((π
β V β§ π β V) β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β πΉ β (π
βpm π)) |
27 | 21, 23, 24, 25, 26 | syl22anc 838 |
. . . 4
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β πΉ β (π
βpm π)) |
28 | 20 | mptex 7177 |
. . . . 5
β’ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))) β V |
29 | 28 | a1i 11 |
. . . 4
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))) β V) |
30 | 7, 19, 27, 29 | fvmptd 6959 |
. . 3
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β (πβπΉ) = (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π)))) |
31 | 30 | ex 414 |
. 2
β’ (π β V β ((πΉ:π΄βΆπ
β§ π΄ β π) β (πβπΉ) = (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))))) |
32 | | 0fv 6890 |
. . . 4
β’
(β
βπΉ) =
β
|
33 | | fvprc 6838 |
. . . . . 6
β’ (Β¬
π β V β
(mRSubstβπ) =
β
) |
34 | 4, 33 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β π = β
) |
35 | 34 | fveq1d 6848 |
. . . 4
β’ (Β¬
π β V β (πβπΉ) = (β
βπΉ)) |
36 | | fvprc 6838 |
. . . . . . 7
β’ (Β¬
π β V β
(mRExβπ) =
β
) |
37 | 3, 36 | eqtrid 2785 |
. . . . . 6
β’ (Β¬
π β V β π
= β
) |
38 | 37 | mpteq1d 5204 |
. . . . 5
β’ (Β¬
π β V β (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))) = (π β β
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π)))) |
39 | | mpt0 6647 |
. . . . 5
β’ (π β β
β¦ (πΊ Ξ£g
((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))) = β
|
40 | 38, 39 | eqtrdi 2789 |
. . . 4
β’ (Β¬
π β V β (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))) = β
) |
41 | 32, 35, 40 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β (πβπΉ) = (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π)))) |
42 | 41 | a1d 25 |
. 2
β’ (Β¬
π β V β ((πΉ:π΄βΆπ
β§ π΄ β π) β (πβπΉ) = (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))))) |
43 | 31, 42 | pm2.61i 182 |
1
β’ ((πΉ:π΄βΆπ
β§ π΄ β π) β (πβπΉ) = (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π)))) |