Step | Hyp | Ref
| Expression |
1 | | mbflim.1 |
. . 3
β’ π =
(β€β₯βπ) |
2 | | mbflim.2 |
. . 3
β’ (π β π β β€) |
3 | | mbflim.4 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) |
4 | 1 | fvexi 6861 |
. . . . . 6
β’ π β V |
5 | 4 | mptex 7178 |
. . . . 5
β’ (π β π β¦ (ββπ΅)) β V |
6 | 5 | a1i 11 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π β π β¦ (ββπ΅)) β V) |
7 | 2 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π΄) β π β β€) |
8 | | mbflim.5 |
. . . . . . . 8
β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) |
9 | | mbflim.6 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β π) |
10 | 9 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π₯ β π΄) β π΅ β π) |
11 | 8, 10 | mbfmptcl 25016 |
. . . . . . 7
β’ (((π β§ π β π) β§ π₯ β π΄) β π΅ β β) |
12 | 11 | an32s 651 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ π β π) β π΅ β β) |
13 | 12 | fmpttd 7068 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅):πβΆβ) |
14 | 13 | ffvelcdmda 7040 |
. . . 4
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ π΅)βπ) β β) |
15 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π β π) β π β π) |
16 | 12 | recld 15086 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π β π) β (ββπ΅) β β) |
17 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β π β¦ (ββπ΅)) = (π β π β¦ (ββπ΅)) |
18 | 17 | fvmpt2 6964 |
. . . . . . . . 9
β’ ((π β π β§ (ββπ΅) β β) β ((π β π β¦ (ββπ΅))βπ) = (ββπ΅)) |
19 | 15, 16, 18 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ (ββπ΅))βπ) = (ββπ΅)) |
20 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π β π β¦ π΅) = (π β π β¦ π΅) |
21 | 20 | fvmpt2 6964 |
. . . . . . . . . 10
β’ ((π β π β§ π΅ β β) β ((π β π β¦ π΅)βπ) = π΅) |
22 | 15, 12, 21 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ π΅)βπ) = π΅) |
23 | 22 | fveq2d 6851 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π) β (ββ((π β π β¦ π΅)βπ)) = (ββπ΅)) |
24 | 19, 23 | eqtr4d 2780 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
25 | 24 | ralrimiva 3144 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β βπ β π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
26 | | nffvmpt1 6858 |
. . . . . . . 8
β’
β²π((π β π β¦ (ββπ΅))βπ) |
27 | | nfcv 2908 |
. . . . . . . . 9
β’
β²πβ |
28 | | nffvmpt1 6858 |
. . . . . . . . 9
β’
β²π((π β π β¦ π΅)βπ) |
29 | 27, 28 | nffv 6857 |
. . . . . . . 8
β’
β²π(ββ((π β π β¦ π΅)βπ)) |
30 | 26, 29 | nfeq 2921 |
. . . . . . 7
β’
β²π((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) |
31 | | nfv 1918 |
. . . . . . 7
β’
β²π((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) |
32 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β ((π β π β¦ (ββπ΅))βπ) = ((π β π β¦ (ββπ΅))βπ)) |
33 | | 2fveq3 6852 |
. . . . . . . 8
β’ (π = π β (ββ((π β π β¦ π΅)βπ)) = (ββ((π β π β¦ π΅)βπ))) |
34 | 32, 33 | eqeq12d 2753 |
. . . . . . 7
β’ (π = π β (((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) β ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)))) |
35 | 30, 31, 34 | cbvralw 3292 |
. . . . . 6
β’
(βπ β
π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) β βπ β π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
36 | 25, 35 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β π΄) β βπ β π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
37 | 36 | r19.21bi 3237 |
. . . 4
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
38 | 1, 3, 6, 7, 14, 37 | climre 15495 |
. . 3
β’ ((π β§ π₯ β π΄) β (π β π β¦ (ββπ΅)) β (ββπΆ)) |
39 | 11 | ismbfcn2 25018 |
. . . . 5
β’ ((π β§ π β π) β ((π₯ β π΄ β¦ π΅) β MblFn β ((π₯ β π΄ β¦ (ββπ΅)) β MblFn β§ (π₯ β π΄ β¦ (ββπ΅)) β MblFn))) |
40 | 8, 39 | mpbid 231 |
. . . 4
β’ ((π β§ π β π) β ((π₯ β π΄ β¦ (ββπ΅)) β MblFn β§ (π₯ β π΄ β¦ (ββπ΅)) β MblFn)) |
41 | 40 | simpld 496 |
. . 3
β’ ((π β§ π β π) β (π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
42 | 11 | anasss 468 |
. . . 4
β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) |
43 | 42 | recld 15086 |
. . 3
β’ ((π β§ (π β π β§ π₯ β π΄)) β (ββπ΅) β β) |
44 | 1, 2, 38, 41, 43 | mbflimlem 25047 |
. 2
β’ (π β (π₯ β π΄ β¦ (ββπΆ)) β MblFn) |
45 | 4 | mptex 7178 |
. . . . 5
β’ (π β π β¦ (ββπ΅)) β V |
46 | 45 | a1i 11 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π β π β¦ (ββπ΅)) β V) |
47 | 12 | imcld 15087 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π β π) β (ββπ΅) β β) |
48 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β π β¦ (ββπ΅)) = (π β π β¦ (ββπ΅)) |
49 | 48 | fvmpt2 6964 |
. . . . . . . . 9
β’ ((π β π β§ (ββπ΅) β β) β ((π β π β¦ (ββπ΅))βπ) = (ββπ΅)) |
50 | 15, 47, 49 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ (ββπ΅))βπ) = (ββπ΅)) |
51 | 22 | fveq2d 6851 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π) β (ββ((π β π β¦ π΅)βπ)) = (ββπ΅)) |
52 | 50, 51 | eqtr4d 2780 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
53 | 52 | ralrimiva 3144 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β βπ β π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
54 | | nffvmpt1 6858 |
. . . . . . . 8
β’
β²π((π β π β¦ (ββπ΅))βπ) |
55 | | nfcv 2908 |
. . . . . . . . 9
β’
β²πβ |
56 | 55, 28 | nffv 6857 |
. . . . . . . 8
β’
β²π(ββ((π β π β¦ π΅)βπ)) |
57 | 54, 56 | nfeq 2921 |
. . . . . . 7
β’
β²π((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) |
58 | | nfv 1918 |
. . . . . . 7
β’
β²π((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) |
59 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β ((π β π β¦ (ββπ΅))βπ) = ((π β π β¦ (ββπ΅))βπ)) |
60 | | 2fveq3 6852 |
. . . . . . . 8
β’ (π = π β (ββ((π β π β¦ π΅)βπ)) = (ββ((π β π β¦ π΅)βπ))) |
61 | 59, 60 | eqeq12d 2753 |
. . . . . . 7
β’ (π = π β (((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) β ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)))) |
62 | 57, 58, 61 | cbvralw 3292 |
. . . . . 6
β’
(βπ β
π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ)) β βπ β π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
63 | 53, 62 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β π΄) β βπ β π ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
64 | 63 | r19.21bi 3237 |
. . . 4
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ (ββπ΅))βπ) = (ββ((π β π β¦ π΅)βπ))) |
65 | 1, 3, 46, 7, 14, 64 | climim 15496 |
. . 3
β’ ((π β§ π₯ β π΄) β (π β π β¦ (ββπ΅)) β (ββπΆ)) |
66 | 40 | simprd 497 |
. . 3
β’ ((π β§ π β π) β (π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
67 | 42 | imcld 15087 |
. . 3
β’ ((π β§ (π β π β§ π₯ β π΄)) β (ββπ΅) β β) |
68 | 1, 2, 65, 66, 67 | mbflimlem 25047 |
. 2
β’ (π β (π₯ β π΄ β¦ (ββπΆ)) β MblFn) |
69 | | climcl 15388 |
. . . 4
β’ ((π β π β¦ π΅) β πΆ β πΆ β β) |
70 | 3, 69 | syl 17 |
. . 3
β’ ((π β§ π₯ β π΄) β πΆ β β) |
71 | 70 | ismbfcn2 25018 |
. 2
β’ (π β ((π₯ β π΄ β¦ πΆ) β MblFn β ((π₯ β π΄ β¦ (ββπΆ)) β MblFn β§ (π₯ β π΄ β¦ (ββπΆ)) β MblFn))) |
72 | 44, 68, 71 | mpbir2and 712 |
1
β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) |