Step | Hyp | Ref
| Expression |
1 | | liminfequzmpt2.j |
. . . . . . . . 9
β’
β²ππ |
2 | | liminfequzmpt2.a |
. . . . . . . . . . . . . . 15
β’ π΄ =
(β€β₯βπ) |
3 | | liminfequzmpt2.k |
. . . . . . . . . . . . . . 15
β’ (π β πΎ β π΄) |
4 | 2, 3 | uzssd2 43738 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπΎ) β π΄) |
5 | 4 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπΎ)) β
(β€β₯βπΎ) β π΄) |
6 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπΎ)) β π β (β€β₯βπΎ)) |
7 | 5, 6 | sseldd 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπΎ)) β π β π΄) |
8 | | liminfequzmpt2.c |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπΎ)) β πΆ β π) |
9 | 8 | elexd 3464 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπΎ)) β πΆ β V) |
10 | 7, 9 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπΎ)) β (π β π΄ β§ πΆ β V)) |
11 | | rabid 3426 |
. . . . . . . . . . 11
β’ (π β {π β π΄ β£ πΆ β V} β (π β π΄ β§ πΆ β V)) |
12 | 10, 11 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπΎ)) β π β {π β π΄ β£ πΆ β V}) |
13 | 12 | ex 414 |
. . . . . . . . 9
β’ (π β (π β (β€β₯βπΎ) β π β {π β π΄ β£ πΆ β V})) |
14 | 1, 13 | ralrimi 3239 |
. . . . . . . 8
β’ (π β βπ β (β€β₯βπΎ)π β {π β π΄ β£ πΆ β V}) |
15 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π(β€β₯βπΎ) |
16 | | nfrab1 3425 |
. . . . . . . . 9
β’
β²π{π β π΄ β£ πΆ β V} |
17 | 15, 16 | dfss3f 3936 |
. . . . . . . 8
β’
((β€β₯βπΎ) β {π β π΄ β£ πΆ β V} β βπ β (β€β₯βπΎ)π β {π β π΄ β£ πΆ β V}) |
18 | 14, 17 | sylibr 233 |
. . . . . . 7
β’ (π β
(β€β₯βπΎ) β {π β π΄ β£ πΆ β V}) |
19 | 16, 15 | resmptf 5994 |
. . . . . . 7
β’
((β€β₯βπΎ) β {π β π΄ β£ πΆ β V} β ((π β {π β π΄ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ)) = (π β (β€β₯βπΎ) β¦ πΆ)) |
20 | 18, 19 | syl 17 |
. . . . . 6
β’ (π β ((π β {π β π΄ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ)) = (π β (β€β₯βπΎ) β¦ πΆ)) |
21 | 20 | eqcomd 2739 |
. . . . 5
β’ (π β (π β (β€β₯βπΎ) β¦ πΆ) = ((π β {π β π΄ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ))) |
22 | 21 | fveq2d 6847 |
. . . 4
β’ (π β (lim infβ(π β
(β€β₯βπΎ) β¦ πΆ)) = (lim infβ((π β {π β π΄ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ)))) |
23 | 2, 3 | eluzelz2d 43734 |
. . . . 5
β’ (π β πΎ β β€) |
24 | | eqid 2733 |
. . . . 5
β’
(β€β₯βπΎ) = (β€β₯βπΎ) |
25 | | liminfequzmpt2.o |
. . . . . . . 8
β’
β²ππ΄ |
26 | 2 | fvexi 6857 |
. . . . . . . 8
β’ π΄ β V |
27 | 25, 26 | rabexf 43432 |
. . . . . . 7
β’ {π β π΄ β£ πΆ β V} β V |
28 | 16, 27 | mptexf 43550 |
. . . . . 6
β’ (π β {π β π΄ β£ πΆ β V} β¦ πΆ) β V |
29 | 28 | a1i 11 |
. . . . 5
β’ (π β (π β {π β π΄ β£ πΆ β V} β¦ πΆ) β V) |
30 | | eqid 2733 |
. . . . . . . 8
β’ (π β {π β π΄ β£ πΆ β V} β¦ πΆ) = (π β {π β π΄ β£ πΆ β V} β¦ πΆ) |
31 | 16, 30 | dmmptssf 43544 |
. . . . . . 7
β’ dom
(π β {π β π΄ β£ πΆ β V} β¦ πΆ) β {π β π΄ β£ πΆ β V} |
32 | 25 | ssrab2f 43415 |
. . . . . . . 8
β’ {π β π΄ β£ πΆ β V} β π΄ |
33 | | uzssz 12789 |
. . . . . . . . 9
β’
(β€β₯βπ) β β€ |
34 | 2, 33 | eqsstri 3979 |
. . . . . . . 8
β’ π΄ β
β€ |
35 | 32, 34 | sstri 3954 |
. . . . . . 7
β’ {π β π΄ β£ πΆ β V} β β€ |
36 | 31, 35 | sstri 3954 |
. . . . . 6
β’ dom
(π β {π β π΄ β£ πΆ β V} β¦ πΆ) β β€ |
37 | 36 | a1i 11 |
. . . . 5
β’ (π β dom (π β {π β π΄ β£ πΆ β V} β¦ πΆ) β β€) |
38 | 23, 24, 29, 37 | liminfresuz2 44114 |
. . . 4
β’ (π β (lim infβ((π β {π β π΄ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ))) = (lim infβ(π β {π β π΄ β£ πΆ β V} β¦ πΆ))) |
39 | 22, 38 | eqtr2d 2774 |
. . 3
β’ (π β (lim infβ(π β {π β π΄ β£ πΆ β V} β¦ πΆ)) = (lim infβ(π β (β€β₯βπΎ) β¦ πΆ))) |
40 | | liminfequzmpt2.b |
. . . . . . . . . . . . . . 15
β’ π΅ =
(β€β₯βπ) |
41 | | liminfequzmpt2.e |
. . . . . . . . . . . . . . 15
β’ (π β πΎ β π΅) |
42 | 40, 41 | uzssd2 43738 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπΎ) β π΅) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπΎ)) β
(β€β₯βπΎ) β π΅) |
44 | 43, 6 | sseldd 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπΎ)) β π β π΅) |
45 | 44, 9 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπΎ)) β (π β π΅ β§ πΆ β V)) |
46 | | rabid 3426 |
. . . . . . . . . . 11
β’ (π β {π β π΅ β£ πΆ β V} β (π β π΅ β§ πΆ β V)) |
47 | 45, 46 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπΎ)) β π β {π β π΅ β£ πΆ β V}) |
48 | 47 | ex 414 |
. . . . . . . . 9
β’ (π β (π β (β€β₯βπΎ) β π β {π β π΅ β£ πΆ β V})) |
49 | 1, 48 | ralrimi 3239 |
. . . . . . . 8
β’ (π β βπ β (β€β₯βπΎ)π β {π β π΅ β£ πΆ β V}) |
50 | | nfrab1 3425 |
. . . . . . . . 9
β’
β²π{π β π΅ β£ πΆ β V} |
51 | 15, 50 | dfss3f 3936 |
. . . . . . . 8
β’
((β€β₯βπΎ) β {π β π΅ β£ πΆ β V} β βπ β (β€β₯βπΎ)π β {π β π΅ β£ πΆ β V}) |
52 | 49, 51 | sylibr 233 |
. . . . . . 7
β’ (π β
(β€β₯βπΎ) β {π β π΅ β£ πΆ β V}) |
53 | 50, 15 | resmptf 5994 |
. . . . . . 7
β’
((β€β₯βπΎ) β {π β π΅ β£ πΆ β V} β ((π β {π β π΅ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ)) = (π β (β€β₯βπΎ) β¦ πΆ)) |
54 | 52, 53 | syl 17 |
. . . . . 6
β’ (π β ((π β {π β π΅ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ)) = (π β (β€β₯βπΎ) β¦ πΆ)) |
55 | 54 | eqcomd 2739 |
. . . . 5
β’ (π β (π β (β€β₯βπΎ) β¦ πΆ) = ((π β {π β π΅ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ))) |
56 | 55 | fveq2d 6847 |
. . . 4
β’ (π β (lim infβ(π β
(β€β₯βπΎ) β¦ πΆ)) = (lim infβ((π β {π β π΅ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ)))) |
57 | | liminfequzmpt2.p |
. . . . . . . 8
β’
β²ππ΅ |
58 | 40 | fvexi 6857 |
. . . . . . . 8
β’ π΅ β V |
59 | 57, 58 | rabexf 43432 |
. . . . . . 7
β’ {π β π΅ β£ πΆ β V} β V |
60 | 50, 59 | mptexf 43550 |
. . . . . 6
β’ (π β {π β π΅ β£ πΆ β V} β¦ πΆ) β V |
61 | 60 | a1i 11 |
. . . . 5
β’ (π β (π β {π β π΅ β£ πΆ β V} β¦ πΆ) β V) |
62 | | eqid 2733 |
. . . . . . . 8
β’ (π β {π β π΅ β£ πΆ β V} β¦ πΆ) = (π β {π β π΅ β£ πΆ β V} β¦ πΆ) |
63 | 50, 62 | dmmptssf 43544 |
. . . . . . 7
β’ dom
(π β {π β π΅ β£ πΆ β V} β¦ πΆ) β {π β π΅ β£ πΆ β V} |
64 | 57 | ssrab2f 43415 |
. . . . . . . 8
β’ {π β π΅ β£ πΆ β V} β π΅ |
65 | | uzssz 12789 |
. . . . . . . . 9
β’
(β€β₯βπ) β β€ |
66 | 40, 65 | eqsstri 3979 |
. . . . . . . 8
β’ π΅ β
β€ |
67 | 64, 66 | sstri 3954 |
. . . . . . 7
β’ {π β π΅ β£ πΆ β V} β β€ |
68 | 63, 67 | sstri 3954 |
. . . . . 6
β’ dom
(π β {π β π΅ β£ πΆ β V} β¦ πΆ) β β€ |
69 | 68 | a1i 11 |
. . . . 5
β’ (π β dom (π β {π β π΅ β£ πΆ β V} β¦ πΆ) β β€) |
70 | 23, 24, 61, 69 | liminfresuz2 44114 |
. . . 4
β’ (π β (lim infβ((π β {π β π΅ β£ πΆ β V} β¦ πΆ) βΎ
(β€β₯βπΎ))) = (lim infβ(π β {π β π΅ β£ πΆ β V} β¦ πΆ))) |
71 | 56, 70 | eqtr2d 2774 |
. . 3
β’ (π β (lim infβ(π β {π β π΅ β£ πΆ β V} β¦ πΆ)) = (lim infβ(π β (β€β₯βπΎ) β¦ πΆ))) |
72 | 39, 71 | eqtr4d 2776 |
. 2
β’ (π β (lim infβ(π β {π β π΄ β£ πΆ β V} β¦ πΆ)) = (lim infβ(π β {π β π΅ β£ πΆ β V} β¦ πΆ))) |
73 | | eqid 2733 |
. . . . 5
β’ {π β π΄ β£ πΆ β V} = {π β π΄ β£ πΆ β V} |
74 | 25, 73 | mptssid 43554 |
. . . 4
β’ (π β π΄ β¦ πΆ) = (π β {π β π΄ β£ πΆ β V} β¦ πΆ) |
75 | 74 | fveq2i 6846 |
. . 3
β’ (lim
infβ(π β π΄ β¦ πΆ)) = (lim infβ(π β {π β π΄ β£ πΆ β V} β¦ πΆ)) |
76 | 75 | a1i 11 |
. 2
β’ (π β (lim infβ(π β π΄ β¦ πΆ)) = (lim infβ(π β {π β π΄ β£ πΆ β V} β¦ πΆ))) |
77 | | eqid 2733 |
. . . . 5
β’ {π β π΅ β£ πΆ β V} = {π β π΅ β£ πΆ β V} |
78 | 57, 77 | mptssid 43554 |
. . . 4
β’ (π β π΅ β¦ πΆ) = (π β {π β π΅ β£ πΆ β V} β¦ πΆ) |
79 | 78 | fveq2i 6846 |
. . 3
β’ (lim
infβ(π β π΅ β¦ πΆ)) = (lim infβ(π β {π β π΅ β£ πΆ β V} β¦ πΆ)) |
80 | 79 | a1i 11 |
. 2
β’ (π β (lim infβ(π β π΅ β¦ πΆ)) = (lim infβ(π β {π β π΅ β£ πΆ β V} β¦ πΆ))) |
81 | 72, 76, 80 | 3eqtr4d 2783 |
1
β’ (π β (lim infβ(π β π΄ β¦ πΆ)) = (lim infβ(π β π΅ β¦ πΆ))) |