Step | Hyp | Ref
| Expression |
1 | | pimdecfgtioo.y |
. . . . . . 7
β’ π = {π₯ β π΄ β£ π
< (πΉβπ₯)} |
2 | | ssrab2 4076 |
. . . . . . 7
β’ {π₯ β π΄ β£ π
< (πΉβπ₯)} β π΄ |
3 | 1, 2 | eqsstri 4015 |
. . . . . 6
β’ π β π΄ |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β π β π΄) |
5 | | pimdecfgtioo.a |
. . . . 5
β’ (π β π΄ β β) |
6 | 4, 5 | sstrd 3991 |
. . . 4
β’ (π β π β β) |
7 | | pimdecfgtioo.c |
. . . 4
β’ π = sup(π, β*, <
) |
8 | | pimdecfgtioo.e |
. . . 4
β’ (π β Β¬ π β π) |
9 | | pimdecfgtioo.i |
. . . 4
β’ πΌ = (-β(,)π) |
10 | 6, 7, 8, 9 | ressioosup 44566 |
. . 3
β’ (π β π β πΌ) |
11 | 10, 4 | ssind 4231 |
. 2
β’ (π β π β (πΌ β© π΄)) |
12 | | pimdecfgtioo.x |
. . . 4
β’
β²π₯π |
13 | | elinel2 4195 |
. . . . . . . 8
β’ (π₯ β (πΌ β© π΄) β π₯ β π΄) |
14 | 13 | adantl 480 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π΄) |
15 | | mnfxr 11275 |
. . . . . . . . . . 11
β’ -β
β β* |
16 | 15 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β -β β
β*) |
17 | | ressxr 11262 |
. . . . . . . . . . . . . 14
β’ β
β β* |
18 | 6, 17 | sstrdi 3993 |
. . . . . . . . . . . . 13
β’ (π β π β
β*) |
19 | 18 | supxrcld 44097 |
. . . . . . . . . . . 12
β’ (π β sup(π, β*, < ) β
β*) |
20 | 7, 19 | eqeltrid 2835 |
. . . . . . . . . . 11
β’ (π β π β
β*) |
21 | 20 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β
β*) |
22 | | elinel1 4194 |
. . . . . . . . . . . 12
β’ (π₯ β (πΌ β© π΄) β π₯ β πΌ) |
23 | 22, 9 | eleqtrdi 2841 |
. . . . . . . . . . 11
β’ (π₯ β (πΌ β© π΄) β π₯ β (-β(,)π)) |
24 | 23 | adantl 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β (-β(,)π)) |
25 | | iooltub 44521 |
. . . . . . . . . 10
β’
((-β β β* β§ π β β* β§ π₯ β (-β(,)π)) β π₯ < π) |
26 | 16, 21, 24, 25 | syl3anc 1369 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ < π) |
27 | 26 | adantr 479 |
. . . . . . . 8
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β π₯ < π) |
28 | | simpr 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β Β¬ π
< (πΉβπ₯)) |
29 | | pimdecfgtioo.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:π΄βΆβ*) |
30 | 29 | adantr 479 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (πΌ β© π΄)) β πΉ:π΄βΆβ*) |
31 | 30, 14 | ffvelcdmd 7086 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ₯) β
β*) |
32 | 31 | adantr 479 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β (πΉβπ₯) β
β*) |
33 | | pimdecfgtioo.r |
. . . . . . . . . . . . . . . 16
β’ (π β π
β
β*) |
34 | 33 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
β
β*) |
35 | 34 | adantr 479 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β π
β
β*) |
36 | 32, 35 | xrlenltd 11284 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β ((πΉβπ₯) β€ π
β Β¬ π
< (πΉβπ₯))) |
37 | 28, 36 | mpbird 256 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β (πΉβπ₯) β€ π
) |
38 | | pimdecfgtioo.h |
. . . . . . . . . . . . . . 15
β’
β²π¦π |
39 | | nfv 1915 |
. . . . . . . . . . . . . . 15
β’
β²π¦ π₯ β (πΌ β© π΄) |
40 | 38, 39 | nfan 1900 |
. . . . . . . . . . . . . 14
β’
β²π¦(π β§ π₯ β (πΌ β© π΄)) |
41 | | nfv 1915 |
. . . . . . . . . . . . . 14
β’
β²π¦(πΉβπ₯) β€ π
|
42 | 40, 41 | nfan 1900 |
. . . . . . . . . . . . 13
β’
β²π¦((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) |
43 | | fveq2 6890 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
44 | 43 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β (π
< (πΉβπ₯) β π
< (πΉβπ¦))) |
45 | 44, 1 | elrab2 3685 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π β (π¦ β π΄ β§ π
< (πΉβπ¦))) |
46 | 45 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β π β (π¦ β π΄ β§ π
< (πΉβπ¦))) |
47 | 46 | simprd 494 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π β π
< (πΉβπ¦)) |
48 | 47 | ad2antlr 723 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π
< (πΉβπ¦)) |
49 | 5 | adantr 479 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (πΌ β© π΄)) β π΄ β β) |
50 | 49, 14 | sseldd 3982 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β β) |
51 | 50 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ β β) |
52 | 6 | sselda 3981 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β π) β π¦ β β) |
53 | 52 | ad4ant13 747 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π¦ β β) |
54 | | simpr 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β Β¬ π¦ β€ π₯) |
55 | 51, 53 | ltnled 11365 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β (π₯ < π¦ β Β¬ π¦ β€ π₯)) |
56 | 54, 55 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ < π¦) |
57 | 51, 53, 56 | ltled 11366 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ β€ π¦) |
58 | 57 | adantllr 715 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β π₯ β€ π¦) |
59 | 29 | adantr 479 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β π) β πΉ:π΄βΆβ*) |
60 | 4 | sselda 3981 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β π) β π¦ β π΄) |
61 | 59, 60 | ffvelcdmd 7086 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β π) β (πΉβπ¦) β
β*) |
62 | 61 | ad5ant14 754 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ¦) β
β*) |
63 | 31 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ₯) β
β*) |
64 | 34 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β π
β
β*) |
65 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β π₯ β€ π¦) |
66 | | pimdecfgtioo.d |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
67 | | rspa 3243 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((βπ₯ β
π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯)) β§ π₯ β π΄) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
68 | 66, 13, 67 | syl2an 594 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (πΌ β© π΄)) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
69 | 68 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
70 | 60 | ad4ant13 747 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β π¦ β π΄) |
71 | | rspa 3243 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((βπ¦ β
π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯)) β§ π¦ β π΄) β (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
72 | 69, 70, 71 | syl2anc 582 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
73 | 65, 72 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ¦) β€ (πΉβπ₯)) |
74 | 73 | adantllr 715 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ¦) β€ (πΉβπ₯)) |
75 | | simpllr 772 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ₯) β€ π
) |
76 | 62, 63, 64, 74, 75 | xrletrd 13145 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β (πΉβπ¦) β€ π
) |
77 | 62, 64 | xrlenltd 11284 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β ((πΉβπ¦) β€ π
β Β¬ π
< (πΉβπ¦))) |
78 | 76, 77 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ π₯ β€ π¦) β Β¬ π
< (πΉβπ¦)) |
79 | 58, 78 | syldan 589 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β§ Β¬ π¦ β€ π₯) β Β¬ π
< (πΉβπ¦)) |
80 | 48, 79 | condan 814 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β§ π¦ β π) β π¦ β€ π₯) |
81 | 80 | ex 411 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β (π¦ β π β π¦ β€ π₯)) |
82 | 42, 81 | ralrimi 3252 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ (πΉβπ₯) β€ π
) β βπ¦ β π π¦ β€ π₯) |
83 | 37, 82 | syldan 589 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β βπ¦ β π π¦ β€ π₯) |
84 | 18 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β
β*) |
85 | 17, 50 | sselid 3979 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β β*) |
86 | | supxrleub 13309 |
. . . . . . . . . . . . 13
β’ ((π β β*
β§ π₯ β
β*) β (sup(π, β*, < ) β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
87 | 84, 85, 86 | syl2anc 582 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (πΌ β© π΄)) β (sup(π, β*, < ) β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
88 | 87 | adantr 479 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β (sup(π, β*, < ) β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
89 | 83, 88 | mpbird 256 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β sup(π, β*, < ) β€ π₯) |
90 | 7, 89 | eqbrtrid 5182 |
. . . . . . . . 9
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β π β€ π₯) |
91 | 21 | adantr 479 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β π β
β*) |
92 | 85 | adantr 479 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β π₯ β β*) |
93 | 91, 92 | xrlenltd 11284 |
. . . . . . . . 9
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β (π β€ π₯ β Β¬ π₯ < π)) |
94 | 90, 93 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ π₯ β (πΌ β© π΄)) β§ Β¬ π
< (πΉβπ₯)) β Β¬ π₯ < π) |
95 | 27, 94 | condan 814 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
< (πΉβπ₯)) |
96 | 14, 95 | jca 510 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β© π΄)) β (π₯ β π΄ β§ π
< (πΉβπ₯))) |
97 | 1 | reqabi 3452 |
. . . . . 6
β’ (π₯ β π β (π₯ β π΄ β§ π
< (πΉβπ₯))) |
98 | 96, 97 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π) |
99 | 98 | ex 411 |
. . . 4
β’ (π β (π₯ β (πΌ β© π΄) β π₯ β π)) |
100 | 12, 99 | ralrimi 3252 |
. . 3
β’ (π β βπ₯ β (πΌ β© π΄)π₯ β π) |
101 | | nfcv 2901 |
. . . 4
β’
β²π₯(πΌ β© π΄) |
102 | | nfrab1 3449 |
. . . . 5
β’
β²π₯{π₯ β π΄ β£ π
< (πΉβπ₯)} |
103 | 1, 102 | nfcxfr 2899 |
. . . 4
β’
β²π₯π |
104 | 101, 103 | dfss3f 3972 |
. . 3
β’ ((πΌ β© π΄) β π β βπ₯ β (πΌ β© π΄)π₯ β π) |
105 | 100, 104 | sylibr 233 |
. 2
β’ (π β (πΌ β© π΄) β π) |
106 | 11, 105 | eqssd 3998 |
1
β’ (π β π = (πΌ β© π΄)) |