Step | Hyp | Ref
| Expression |
1 | | fnlimfvre.x |
. . 3
β’ (π β π β π·) |
2 | | fnlimfvre.d |
. . . . . 6
β’ π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
3 | | nfcv 2904 |
. . . . . . . 8
β’
β²π₯π |
4 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π₯(β€β₯βπ) |
5 | | fnlimfvre.n |
. . . . . . . . . . 11
β’
β²π₯πΉ |
6 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π₯π |
7 | 5, 6 | nffv 6853 |
. . . . . . . . . 10
β’
β²π₯(πΉβπ) |
8 | 7 | nfdm 5907 |
. . . . . . . . 9
β’
β²π₯dom
(πΉβπ) |
9 | 4, 8 | nfiin 4986 |
. . . . . . . 8
β’
β²π₯β© π β
(β€β₯βπ)dom (πΉβπ) |
10 | 3, 9 | nfiun 4985 |
. . . . . . 7
β’
β²π₯βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
11 | 10 | ssrab2f 43415 |
. . . . . 6
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
12 | 2, 11 | eqsstri 3979 |
. . . . 5
β’ π· β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
13 | 12 | sseli 3941 |
. . . 4
β’ (π β π· β π β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ)) |
14 | | eliun 4959 |
. . . 4
β’ (π β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β βπ β π π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
15 | 13, 14 | sylib 217 |
. . 3
β’ (π β π· β βπ β π π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
16 | 1, 15 | syl 17 |
. 2
β’ (π β βπ β π π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
17 | | nfv 1918 |
. . 3
β’
β²ππ |
18 | | nfv 1918 |
. . 3
β’
β²π( β
β(π β π β¦ ((πΉβπ)βπ))) β β |
19 | | fnlimfvre.p |
. . . . . . 7
β’
β²ππ |
20 | | nfv 1918 |
. . . . . . 7
β’
β²π π β π |
21 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ |
22 | | nfii1 4990 |
. . . . . . . 8
β’
β²πβ© π β
(β€β₯βπ)dom (πΉβπ) |
23 | 21, 22 | nfel 2918 |
. . . . . . 7
β’
β²π π β β© π β (β€β₯βπ)dom (πΉβπ) |
24 | 19, 20, 23 | nf3an 1905 |
. . . . . 6
β’
β²π(π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
25 | | uzssz 12789 |
. . . . . . . 8
β’
(β€β₯βπ) β β€ |
26 | | fnlimfvre.z |
. . . . . . . . . 10
β’ π =
(β€β₯βπ) |
27 | 26 | eleq2i 2826 |
. . . . . . . . 9
β’ (π β π β π β (β€β₯βπ)) |
28 | 27 | biimpi 215 |
. . . . . . . 8
β’ (π β π β π β (β€β₯βπ)) |
29 | 25, 28 | sselid 3943 |
. . . . . . 7
β’ (π β π β π β β€) |
30 | 29 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β π β β€) |
31 | | eqid 2733 |
. . . . . 6
β’
(β€β₯βπ) = (β€β₯βπ) |
32 | 26 | fvexi 6857 |
. . . . . . 7
β’ π β V |
33 | 32 | a1i 11 |
. . . . . 6
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β π β V) |
34 | 26 | uztrn2 12787 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
35 | 34 | ssd 43378 |
. . . . . . 7
β’ (π β π β (β€β₯βπ) β π) |
36 | 35 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β (β€β₯βπ) β π) |
37 | | fvexd 6858 |
. . . . . 6
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β π) β ((πΉβπ)βπ) β V) |
38 | | fvexd 6858 |
. . . . . 6
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β (β€β₯βπ) β V) |
39 | | ssidd 3968 |
. . . . . 6
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β (β€β₯βπ) β
(β€β₯βπ)) |
40 | | fvexd 6858 |
. . . . . 6
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β V) |
41 | | eqidd 2734 |
. . . . . 6
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
42 | 24, 30, 31, 33, 36, 37, 38, 39, 40, 41 | climfveqmpt 43998 |
. . . . 5
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β ( β β(π β π β¦ ((πΉβπ)βπ))) = ( β β(π β (β€β₯βπ) β¦ ((πΉβπ)βπ)))) |
43 | 2 | eleq2i 2826 |
. . . . . . . . . . . . 13
β’ (π β π· β π β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β }) |
44 | 43 | biimpi 215 |
. . . . . . . . . . . 12
β’ (π β π· β π β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β }) |
45 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π₯π |
46 | 7, 45 | nffv 6853 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯((πΉβπ)βπ) |
47 | 3, 46 | nfmpt 5213 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(π β π β¦ ((πΉβπ)βπ)) |
48 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²π₯dom
β |
49 | 47, 48 | nfel 2918 |
. . . . . . . . . . . . . . 15
β’
β²π₯(π β π β¦ ((πΉβπ)βπ)) β dom β |
50 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ)) |
51 | 50 | mpteq2dv 5208 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ))) |
52 | 51 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((π β π β¦ ((πΉβπ)βπ₯)) β dom β β (π β π β¦ ((πΉβπ)βπ)) β dom β )) |
53 | 45, 10, 49, 52 | elrabf 3642 |
. . . . . . . . . . . . . 14
β’ (π β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } β (π β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β§ (π β π β¦ ((πΉβπ)βπ)) β dom β )) |
54 | 53 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } β (π β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β§ (π β π β¦ ((πΉβπ)βπ)) β dom β )) |
55 | 54 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } β (π β π β¦ ((πΉβπ)βπ)) β dom β ) |
56 | 44, 55 | syl 17 |
. . . . . . . . . . 11
β’ (π β π· β (π β π β¦ ((πΉβπ)βπ)) β dom β ) |
57 | 56 | adantr 482 |
. . . . . . . . . 10
β’ ((π β π· β§ π β π) β (π β π β¦ ((πΉβπ)βπ)) β dom β ) |
58 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . 16
β’
β²π(π β π β¦ ((πΉβπ)βπ₯)) |
59 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²πdom
β |
60 | 58, 59 | nfel 2918 |
. . . . . . . . . . . . . . 15
β’
β²π(π β π β¦ ((πΉβπ)βπ₯)) β dom β |
61 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π π β π |
62 | 61 | nfci 2887 |
. . . . . . . . . . . . . . . 16
β’
β²ππ |
63 | 62, 22 | nfiun 4985 |
. . . . . . . . . . . . . . 15
β’
β²πβͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
64 | 60, 63 | nfrabw 3439 |
. . . . . . . . . . . . . 14
β’
β²π{π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
65 | 2, 64 | nfcxfr 2902 |
. . . . . . . . . . . . 13
β’
β²ππ· |
66 | 21, 65 | nfel 2918 |
. . . . . . . . . . . 12
β’
β²π π β π· |
67 | 66, 20 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π(π β π· β§ π β π) |
68 | 29 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β π· β§ π β π) β π β β€) |
69 | 32 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β π· β§ π β π) β π β V) |
70 | 35 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β π· β§ π β π) β (β€β₯βπ) β π) |
71 | | fvexd 6858 |
. . . . . . . . . . 11
β’ (((π β π· β§ π β π) β§ π β π) β ((πΉβπ)βπ) β V) |
72 | | fvexd 6858 |
. . . . . . . . . . 11
β’ ((π β π· β§ π β π) β (β€β₯βπ) β V) |
73 | | ssidd 3968 |
. . . . . . . . . . 11
β’ ((π β π· β§ π β π) β (β€β₯βπ) β
(β€β₯βπ)) |
74 | | fvexd 6858 |
. . . . . . . . . . 11
β’ (((π β π· β§ π β π) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β V) |
75 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (((π β π· β§ π β π) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
76 | 67, 68, 31, 69, 70, 71, 72, 73, 74, 75 | climeldmeqmpt 43995 |
. . . . . . . . . 10
β’ ((π β π· β§ π β π) β ((π β π β¦ ((πΉβπ)βπ)) β dom β β (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)) β dom β )) |
77 | 57, 76 | mpbid 231 |
. . . . . . . . 9
β’ ((π β π· β§ π β π) β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ)) β dom β ) |
78 | | climdm 15442 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)) β dom β β (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)) β ( β β(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)))) |
79 | 77, 78 | sylib 217 |
. . . . . . . 8
β’ ((π β π· β§ π β π) β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ)) β ( β β(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)))) |
80 | 1, 79 | sylan 581 |
. . . . . . 7
β’ ((π β§ π β π) β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ)) β ( β β(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)))) |
81 | 80 | 3adant3 1133 |
. . . . . 6
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ)) β ( β β(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)))) |
82 | | simpl1 1192 |
. . . . . . 7
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β (β€β₯βπ)) β π) |
83 | | simpl2 1193 |
. . . . . . 7
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β (β€β₯βπ)) β π β π) |
84 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²πdom
(πΉβπ) |
85 | | fnlimfvre.m |
. . . . . . . . . . . . . . 15
β’
β²ππΉ |
86 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
87 | 85, 86 | nffv 6853 |
. . . . . . . . . . . . . 14
β’
β²π(πΉβπ) |
88 | 87 | nfdm 5907 |
. . . . . . . . . . . . 13
β’
β²πdom
(πΉβπ) |
89 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
90 | 89 | dmeqd 5862 |
. . . . . . . . . . . . 13
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
91 | 84, 88, 90 | cbviin 4998 |
. . . . . . . . . . . 12
β’ β© π β (β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ) |
92 | 91 | eleq2i 2826 |
. . . . . . . . . . 11
β’ (π β β© π β (β€β₯βπ)dom (πΉβπ) β π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
93 | 92 | biimpi 215 |
. . . . . . . . . 10
β’ (π β β© π β (β€β₯βπ)dom (πΉβπ) β π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
94 | 93 | adantr 482 |
. . . . . . . . 9
β’ ((π β β© π β (β€β₯βπ)dom (πΉβπ) β§ π β (β€β₯βπ)) β π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
95 | | simpr 486 |
. . . . . . . . 9
β’ ((π β β© π β (β€β₯βπ)dom (πΉβπ) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
96 | | eliinid 43409 |
. . . . . . . . 9
β’ ((π β β© π β (β€β₯βπ)dom (πΉβπ) β§ π β (β€β₯βπ)) β π β dom (πΉβπ)) |
97 | 94, 95, 96 | syl2anc 585 |
. . . . . . . 8
β’ ((π β β© π β (β€β₯βπ)dom (πΉβπ) β§ π β (β€β₯βπ)) β π β dom (πΉβπ)) |
98 | 97 | 3ad2antl3 1188 |
. . . . . . 7
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β (β€β₯βπ)) β π β dom (πΉβπ)) |
99 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
100 | | id 22 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β (β€β₯βπ)) |
101 | | fvexd 6858 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β ((πΉβπ)βπ) β V) |
102 | 87, 21 | nffv 6853 |
. . . . . . . . . . 11
β’
β²π((πΉβπ)βπ) |
103 | 89 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
104 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)) = (π β (β€β₯βπ) β¦ ((πΉβπ)βπ)) |
105 | 86, 102, 103, 104 | fvmptf 6970 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ ((πΉβπ)βπ) β V) β ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ))βπ) = ((πΉβπ)βπ)) |
106 | 100, 101,
105 | syl2anc 585 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ))βπ) = ((πΉβπ)βπ)) |
107 | 106 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β π β§ π β dom (πΉβπ)) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ))βπ) = ((πΉβπ)βπ)) |
108 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
109 | 34 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
110 | 19, 61 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π(π β§ π β π) |
111 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²πβ |
112 | 87, 88, 111 | nff 6665 |
. . . . . . . . . . . . 13
β’
β²π(πΉβπ):dom (πΉβπ)βΆβ |
113 | 110, 112 | nfim 1900 |
. . . . . . . . . . . 12
β’
β²π((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
114 | | eleq1w 2817 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π β π β π)) |
115 | 114 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β§ π β π) β (π β§ π β π))) |
116 | 89, 90 | feq12d 6657 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ):dom (πΉβπ)βΆβ β (πΉβπ):dom (πΉβπ)βΆβ)) |
117 | 115, 116 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = π β (((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) β ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ))) |
118 | | fnlimfvre.f |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
119 | 113, 117,
118 | chvarfv 2234 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
120 | 108, 109,
119 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ):dom (πΉβπ)βΆβ) |
121 | 120 | 3adantl3 1169 |
. . . . . . . . 9
β’ (((π β§ π β π β§ π β dom (πΉβπ)) β§ π β (β€β₯βπ)) β (πΉβπ):dom (πΉβπ)βΆβ) |
122 | | simpl3 1194 |
. . . . . . . . 9
β’ (((π β§ π β π β§ π β dom (πΉβπ)) β§ π β (β€β₯βπ)) β π β dom (πΉβπ)) |
123 | 121, 122 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((π β§ π β π β§ π β dom (πΉβπ)) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β β) |
124 | 107, 123 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β§ π β π β§ π β dom (πΉβπ)) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ))βπ) β β) |
125 | 82, 83, 98, 99, 124 | syl31anc 1374 |
. . . . . 6
β’ (((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ))βπ) β β) |
126 | 31, 30, 81, 125 | climrecl 15471 |
. . . . 5
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β ( β β(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ))) β β) |
127 | 42, 126 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β π β§ π β β©
π β
(β€β₯βπ)dom (πΉβπ)) β ( β β(π β π β¦ ((πΉβπ)βπ))) β β) |
128 | 127 | 3exp 1120 |
. . 3
β’ (π β (π β π β (π β β©
π β
(β€β₯βπ)dom (πΉβπ) β ( β β(π β π β¦ ((πΉβπ)βπ))) β β))) |
129 | 17, 18, 128 | rexlimd 3248 |
. 2
β’ (π β (βπ β π π β β©
π β
(β€β₯βπ)dom (πΉβπ) β ( β β(π β π β¦ ((πΉβπ)βπ))) β β)) |
130 | 16, 129 | mpd 15 |
1
β’ (π β ( β β(π β π β¦ ((πΉβπ)βπ))) β β) |