Step | Hyp | Ref
| Expression |
1 | | msubffval.v |
. . . . . 6
β’ π = (mVRβπ) |
2 | | msubffval.r |
. . . . . 6
β’ π
= (mRExβπ) |
3 | | msubffval.s |
. . . . . 6
β’ π = (mSubstβπ) |
4 | | msubffval.e |
. . . . . 6
β’ πΈ = (mExβπ) |
5 | | msubffval.o |
. . . . . 6
β’ π = (mRSubstβπ) |
6 | 1, 2, 3, 4, 5 | msubffval 34181 |
. . . . 5
β’ (π β V β π = (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β π = (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |
8 | | simplr 768 |
. . . . . . . 8
β’ ((((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β§ π β πΈ) β π = πΉ) |
9 | 8 | fveq2d 6850 |
. . . . . . 7
β’ ((((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β§ π β πΈ) β (πβπ) = (πβπΉ)) |
10 | 9 | fveq1d 6848 |
. . . . . 6
β’ ((((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β§ π β πΈ) β ((πβπ)β(2nd βπ)) = ((πβπΉ)β(2nd βπ))) |
11 | 10 | opeq2d 4841 |
. . . . 5
β’ ((((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β§ π β πΈ) β β¨(1st βπ), ((πβπ)β(2nd βπ))β© = β¨(1st
βπ), ((πβπΉ)β(2nd βπ))β©) |
12 | 11 | mpteq2dva 5209 |
. . . 4
β’ (((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β§ π = πΉ) β (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©)) |
13 | 2 | fvexi 6860 |
. . . . . . 7
β’ π
β V |
14 | 1 | fvexi 6860 |
. . . . . . 7
β’ π β V |
15 | 13, 14 | pm3.2i 472 |
. . . . . 6
β’ (π
β V β§ π β V) |
16 | 15 | a1i 11 |
. . . . 5
β’ (π β V β (π
β V β§ π β V)) |
17 | | elpm2r 8789 |
. . . . 5
β’ (((π
β V β§ π β V) β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β πΉ β (π
βpm π)) |
18 | 16, 17 | sylan 581 |
. . . 4
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β πΉ β (π
βpm π)) |
19 | 4 | fvexi 6860 |
. . . . . 6
β’ πΈ β V |
20 | 19 | mptex 7177 |
. . . . 5
β’ (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) β
V |
21 | 20 | a1i 11 |
. . . 4
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) β
V) |
22 | 7, 12, 18, 21 | fvmptd 6959 |
. . 3
β’ ((π β V β§ (πΉ:π΄βΆπ
β§ π΄ β π)) β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©)) |
23 | 22 | ex 414 |
. 2
β’ (π β V β ((πΉ:π΄βΆπ
β§ π΄ β π) β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©))) |
24 | | 0fv 6890 |
. . . . 5
β’
(β
βπΉ) =
β
|
25 | | mpt0 6647 |
. . . . 5
β’ (π β β
β¦
β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) =
β
|
26 | 24, 25 | eqtr4i 2764 |
. . . 4
β’
(β
βπΉ) =
(π β β
β¦
β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) |
27 | | fvprc 6838 |
. . . . . 6
β’ (Β¬
π β V β
(mSubstβπ) =
β
) |
28 | 3, 27 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β π = β
) |
29 | 28 | fveq1d 6848 |
. . . 4
β’ (Β¬
π β V β (πβπΉ) = (β
βπΉ)) |
30 | | fvprc 6838 |
. . . . . 6
β’ (Β¬
π β V β
(mExβπ) =
β
) |
31 | 4, 30 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β πΈ = β
) |
32 | 31 | mpteq1d 5204 |
. . . 4
β’ (Β¬
π β V β (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) = (π β β
β¦ β¨(1st
βπ), ((πβπΉ)β(2nd βπ))β©)) |
33 | 26, 29, 32 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©)) |
34 | 33 | a1d 25 |
. 2
β’ (Β¬
π β V β ((πΉ:π΄βΆπ
β§ π΄ β π) β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©))) |
35 | 23, 34 | pm2.61i 182 |
1
β’ ((πΉ:π΄βΆπ
β§ π΄ β π) β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©)) |