Step | Hyp | Ref
| Expression |
1 | | pimincfltioo.y |
. . . . . . 7
β’ π = {π₯ β π΄ β£ (πΉβπ₯) < π
} |
2 | | ssrab2 4038 |
. . . . . . 7
β’ {π₯ β π΄ β£ (πΉβπ₯) < π
} β π΄ |
3 | 1, 2 | eqsstri 3979 |
. . . . . 6
β’ π β π΄ |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β π β π΄) |
5 | | pimincfltioo.a |
. . . . 5
β’ (π β π΄ β β) |
6 | 4, 5 | sstrd 3955 |
. . . 4
β’ (π β π β β) |
7 | | pimincfltioo.c |
. . . 4
β’ π = sup(π, β*, <
) |
8 | | pimincfltioo.e |
. . . 4
β’ (π β Β¬ π β π) |
9 | | pimincfltioo.d |
. . . 4
β’ πΌ = (-β(,)π) |
10 | 6, 7, 8, 9 | ressioosup 43879 |
. . 3
β’ (π β π β πΌ) |
11 | 10, 4 | ssind 4193 |
. 2
β’ (π β π β (πΌ β© π΄)) |
12 | | pimincfltioo.x |
. . . 4
β’
β²π₯π |
13 | | elinel2 4157 |
. . . . . . . 8
β’ (π₯ β (πΌ β© π΄) β π₯ β π΄) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π΄) |
15 | | mnfxr 11217 |
. . . . . . . . . . 11
β’ -β
β β* |
16 | 15 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β -β β
β*) |
17 | | ressxr 11204 |
. . . . . . . . . . . . . 14
β’ β
β β* |
18 | 6, 17 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’ (π β π β
β*) |
19 | 18 | supxrcld 43405 |
. . . . . . . . . . . 12
β’ (π β sup(π, β*, < ) β
β*) |
20 | 7, 19 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β π β
β*) |
21 | 20 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β
β*) |
22 | | elinel1 4156 |
. . . . . . . . . . . 12
β’ (π₯ β (πΌ β© π΄) β π₯ β πΌ) |
23 | 22, 9 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (π₯ β (πΌ β© π΄) β π₯ β (-β(,)π)) |
24 | 23 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β (-β(,)π)) |
25 | | iooltub 43834 |
. . . . . . . . . 10
β’
((-β β β* β§ π β β* β§ π₯ β (-β(,)π)) β π₯ < π) |
26 | 16, 21, 24, 25 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ < π) |
27 | 26 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β π₯ < π) |
28 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β Β¬ (πΉβπ₯) < π
) |
29 | | pimincfltioo.r |
. . . . . . . . . . . . . . . 16
β’ (π β π
β
β*) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
β
β*) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β π
β
β*) |
32 | | pimincfltioo.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:π΄βΆβ*) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (πΌ β© π΄)) β πΉ:π΄βΆβ*) |
34 | 33, 14 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ₯) β
β*) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β (πΉβπ₯) β
β*) |
36 | 31, 35 | xrlenltd 11226 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β (π
β€ (πΉβπ₯) β Β¬ (πΉβπ₯) < π
)) |
37 | 28, 36 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β π
β€ (πΉβπ₯)) |
38 | | pimincfltioo.h |
. . . . . . . . . . . . . . 15
β’
β²π¦π |
39 | | nfv 1918 |
. . . . . . . . . . . . . . 15
β’
β²π¦ π₯ β (πΌ β© π΄) |
40 | 38, 39 | nfan 1903 |
. . . . . . . . . . . . . 14
β’
β²π¦(π β§ π₯ β (πΌ β© π΄)) |
41 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π¦ π
β€ (πΉβπ₯) |
42 | 40, 41 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π¦((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) |
43 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
44 | 43 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β ((πΉβπ₯) < π
β (πΉβπ¦) < π
)) |
45 | 44, 1 | elrab2 3649 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β π β (π¦ β π΄ β§ (πΉβπ¦) < π
)) |
46 | 45 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π β (π¦ β π΄ β§ (πΉβπ¦) < π
)) |
47 | 46 | simprd 497 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β π β (πΉβπ¦) < π
) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β π) β (πΉβπ¦) < π
) |
49 | 48 | ad5ant14 757 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β (πΉβπ¦) < π
) |
50 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (πΌ β© π΄)) β π΄ β β) |
51 | 50, 14 | sseldd 3946 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β β) |
52 | 51 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ β β) |
53 | 6 | sselda 3945 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β π) β π¦ β β) |
54 | 53 | ad5ant14 757 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π¦ β β) |
55 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β Β¬ π¦ β€ π₯) |
56 | 51 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ β β) |
57 | 53 | ad4ant13 750 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π¦ β β) |
58 | 56, 57 | ltnled 11307 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β (π₯ < π¦ β Β¬ π¦ β€ π₯)) |
59 | 55, 58 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ < π¦) |
60 | 59 | adantllr 718 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ < π¦) |
61 | 52, 54, 60 | ltled 11308 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ β€ π¦) |
62 | 30 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β π
β
β*) |
63 | 34 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ₯) β
β*) |
64 | 32 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β π) β πΉ:π΄βΆβ*) |
65 | 4 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β π) β π¦ β π΄) |
66 | 64, 65 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β π) β (πΉβπ¦) β
β*) |
67 | 66 | ad5ant14 757 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ¦) β
β*) |
68 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β π
β€ (πΉβπ₯)) |
69 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π€(((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) |
70 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π§(((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) |
71 | | pimincfltioo.i |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
72 | | breq1 5109 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ = π₯ β (π€ β€ π§ β π₯ β€ π§)) |
73 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ = π₯ β (πΉβπ€) = (πΉβπ₯)) |
74 | 73 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ = π₯ β ((πΉβπ€) β€ (πΉβπ§) β (πΉβπ₯) β€ (πΉβπ§))) |
75 | 72, 74 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ = π₯ β ((π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§)) β (π₯ β€ π§ β (πΉβπ₯) β€ (πΉβπ§)))) |
76 | | breq2 5110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ = π¦ β (π₯ β€ π§ β π₯ β€ π¦)) |
77 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ = π¦ β (πΉβπ§) = (πΉβπ¦)) |
78 | 77 | breq2d 5118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ = π¦ β ((πΉβπ₯) β€ (πΉβπ§) β (πΉβπ₯) β€ (πΉβπ¦))) |
79 | 76, 78 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ = π¦ β ((π₯ β€ π§ β (πΉβπ₯) β€ (πΉβπ§)) β (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)))) |
80 | 75, 79 | cbvral2vw 3226 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ€ β
π΄ βπ§ β π΄ (π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§)) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
81 | 71, 80 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βπ€ β π΄ βπ§ β π΄ (π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§))) |
82 | 81 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β βπ€ β π΄ βπ§ β π΄ (π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§))) |
83 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β π₯ β π΄) |
84 | 65 | ad4ant13 750 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β π¦ β π΄) |
85 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β π₯ β€ π¦) |
86 | 69, 70, 82, 83, 84, 85 | dmrelrnrel 43534 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ₯) β€ (πΉβπ¦)) |
87 | 86 | adantllr 718 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ₯) β€ (πΉβπ¦)) |
88 | 62, 63, 67, 68, 87 | xrletrd 13087 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β π
β€ (πΉβπ¦)) |
89 | 62, 67 | xrlenltd 11226 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β (π
β€ (πΉβπ¦) β Β¬ (πΉβπ¦) < π
)) |
90 | 88, 89 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ π₯ β€ π¦) β Β¬ (πΉβπ¦) < π
) |
91 | 61, 90 | syldan 592 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β Β¬ (πΉβπ¦) < π
) |
92 | 49, 91 | condan 817 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β§ π¦ β π) β π¦ β€ π₯) |
93 | 92 | ex 414 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β (π¦ β π β π¦ β€ π₯)) |
94 | 42, 93 | ralrimi 3239 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ π
β€ (πΉβπ₯)) β βπ¦ β π π¦ β€ π₯) |
95 | 37, 94 | syldan 592 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β βπ¦ β π π¦ β€ π₯) |
96 | 18 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β
β*) |
97 | 17, 51 | sselid 3943 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β β*) |
98 | | supxrleub 13251 |
. . . . . . . . . . . . 13
β’ ((π β β*
β§ π₯ β
β*) β (sup(π, β*, < ) β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
99 | 96, 97, 98 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (πΌ β© π΄)) β (sup(π, β*, < ) β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
100 | 99 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β (sup(π, β*, < ) β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
101 | 95, 100 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β sup(π, β*, < ) β€ π₯) |
102 | 7, 101 | eqbrtrid 5141 |
. . . . . . . . 9
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β π β€ π₯) |
103 | 21 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β π β
β*) |
104 | 97 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β π₯ β β*) |
105 | 103, 104 | xrlenltd 11226 |
. . . . . . . . 9
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β (π β€ π₯ β Β¬ π₯ < π)) |
106 | 102, 105 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ (πΉβπ₯) < π
) β Β¬ π₯ < π) |
107 | 27, 106 | condan 817 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ₯) < π
) |
108 | 14, 107 | jca 513 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β© π΄)) β (π₯ β π΄ β§ (πΉβπ₯) < π
)) |
109 | 1 | reqabi 3428 |
. . . . . 6
β’ (π₯ β π β (π₯ β π΄ β§ (πΉβπ₯) < π
)) |
110 | 108, 109 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π) |
111 | 110 | ex 414 |
. . . 4
β’ (π β (π₯ β (πΌ β© π΄) β π₯ β π)) |
112 | 12, 111 | ralrimi 3239 |
. . 3
β’ (π β βπ₯ β (πΌ β© π΄)π₯ β π) |
113 | | nfcv 2904 |
. . . 4
β’
β²π₯(πΌ β© π΄) |
114 | | nfrab1 3425 |
. . . . 5
β’
β²π₯{π₯ β π΄ β£ (πΉβπ₯) < π
} |
115 | 1, 114 | nfcxfr 2902 |
. . . 4
β’
β²π₯π |
116 | 113, 115 | dfss3f 3936 |
. . 3
β’ ((πΌ β© π΄) β π β βπ₯ β (πΌ β© π΄)π₯ β π) |
117 | 112, 116 | sylibr 233 |
. 2
β’ (π β (πΌ β© π΄) β π) |
118 | 11, 117 | eqssd 3962 |
1
β’ (π β π = (πΌ β© π΄)) |