Step | Hyp | Ref
| Expression |
1 | | fnlimfvre2.g |
. . . 4
β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) |
2 | | fnlimfvre2.d |
. . . . . 6
β’ π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
3 | | nfrab1 3445 |
. . . . . 6
β’
β²π₯{π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
4 | 2, 3 | nfcxfr 2895 |
. . . . 5
β’
β²π₯π· |
5 | | nfcv 2897 |
. . . . 5
β’
β²π§π· |
6 | | nfcv 2897 |
. . . . 5
β’
β²π§(
β β(π β
π β¦ ((πΉβπ)βπ₯))) |
7 | | nfcv 2897 |
. . . . . 6
β’
β²π₯
β |
8 | | nfcv 2897 |
. . . . . . 7
β’
β²π₯π |
9 | | fnlimfvre2.n |
. . . . . . . . 9
β’
β²π₯πΉ |
10 | | nfcv 2897 |
. . . . . . . . 9
β’
β²π₯π |
11 | 9, 10 | nffv 6895 |
. . . . . . . 8
β’
β²π₯(πΉβπ) |
12 | | nfcv 2897 |
. . . . . . . 8
β’
β²π₯π§ |
13 | 11, 12 | nffv 6895 |
. . . . . . 7
β’
β²π₯((πΉβπ)βπ§) |
14 | 8, 13 | nfmpt 5248 |
. . . . . 6
β’
β²π₯(π β π β¦ ((πΉβπ)βπ§)) |
15 | 7, 14 | nffv 6895 |
. . . . 5
β’
β²π₯(
β β(π β
π β¦ ((πΉβπ)βπ§))) |
16 | | fveq2 6885 |
. . . . . . 7
β’ (π₯ = π§ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ§)) |
17 | 16 | mpteq2dv 5243 |
. . . . . 6
β’ (π₯ = π§ β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ§))) |
18 | 17 | fveq2d 6889 |
. . . . 5
β’ (π₯ = π§ β ( β β(π β π β¦ ((πΉβπ)βπ₯))) = ( β β(π β π β¦ ((πΉβπ)βπ§)))) |
19 | 4, 5, 6, 15, 18 | cbvmptf 5250 |
. . . 4
β’ (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) = (π§ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ§)))) |
20 | 1, 19 | eqtri 2754 |
. . 3
β’ πΊ = (π§ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ§)))) |
21 | | fveq2 6885 |
. . . . . 6
β’ (π = π§ β ((πΉβπ)βπ) = ((πΉβπ)βπ§)) |
22 | 21 | mpteq2dv 5243 |
. . . . 5
β’ (π = π§ β (π β π β¦ ((πΉβπ)βπ)) = (π β π β¦ ((πΉβπ)βπ§))) |
23 | | eqcom 2733 |
. . . . . . 7
β’ (π = π§ β π§ = π) |
24 | 23 | imbi1i 349 |
. . . . . 6
β’ ((π = π§ β (π β π β¦ ((πΉβπ)βπ)) = (π β π β¦ ((πΉβπ)βπ§))) β (π§ = π β (π β π β¦ ((πΉβπ)βπ)) = (π β π β¦ ((πΉβπ)βπ§)))) |
25 | | eqcom 2733 |
. . . . . . 7
β’ ((π β π β¦ ((πΉβπ)βπ)) = (π β π β¦ ((πΉβπ)βπ§)) β (π β π β¦ ((πΉβπ)βπ§)) = (π β π β¦ ((πΉβπ)βπ))) |
26 | 25 | imbi2i 336 |
. . . . . 6
β’ ((π§ = π β (π β π β¦ ((πΉβπ)βπ)) = (π β π β¦ ((πΉβπ)βπ§))) β (π§ = π β (π β π β¦ ((πΉβπ)βπ§)) = (π β π β¦ ((πΉβπ)βπ)))) |
27 | 24, 26 | bitri 275 |
. . . . 5
β’ ((π = π§ β (π β π β¦ ((πΉβπ)βπ)) = (π β π β¦ ((πΉβπ)βπ§))) β (π§ = π β (π β π β¦ ((πΉβπ)βπ§)) = (π β π β¦ ((πΉβπ)βπ)))) |
28 | 22, 27 | mpbi 229 |
. . . 4
β’ (π§ = π β (π β π β¦ ((πΉβπ)βπ§)) = (π β π β¦ ((πΉβπ)βπ))) |
29 | 28 | fveq2d 6889 |
. . 3
β’ (π§ = π β ( β β(π β π β¦ ((πΉβπ)βπ§))) = ( β β(π β π β¦ ((πΉβπ)βπ)))) |
30 | | fnlimfvre2.x |
. . 3
β’ (π β π β π·) |
31 | | fvexd 6900 |
. . 3
β’ (π β ( β β(π β π β¦ ((πΉβπ)βπ))) β V) |
32 | 20, 29, 30, 31 | fvmptd3 7015 |
. 2
β’ (π β (πΊβπ) = ( β β(π β π β¦ ((πΉβπ)βπ)))) |
33 | | fnlimfvre2.p |
. . 3
β’
β²ππ |
34 | | fnlimfvre2.m |
. . 3
β’
β²ππΉ |
35 | | fnlimfvre2.z |
. . 3
β’ π =
(β€β₯βπ) |
36 | | fnlimfvre2.f |
. . 3
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
37 | 33, 34, 9, 35, 36, 2, 30 | fnlimfvre 44967 |
. 2
β’ (π β ( β β(π β π β¦ ((πΉβπ)βπ))) β β) |
38 | 32, 37 | eqeltrd 2827 |
1
β’ (π β (πΊβπ) β β) |