Step | Hyp | Ref
| Expression |
1 | | pimdecfgtioc.y |
. . . . . . 7
β’ π = {π₯ β π΄ β£ π
< (πΉβπ₯)} |
2 | | ssrab2 4076 |
. . . . . . 7
β’ {π₯ β π΄ β£ π
< (πΉβπ₯)} β π΄ |
3 | 1, 2 | eqsstri 4015 |
. . . . . 6
β’ π β π΄ |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β π β π΄) |
5 | | pimdecfgtioc.a |
. . . . 5
β’ (π β π΄ β β) |
6 | 4, 5 | sstrd 3991 |
. . . 4
β’ (π β π β β) |
7 | | pimdecfgtioc.c |
. . . 4
β’ π = sup(π, β*, <
) |
8 | | pimdecfgtioc.e |
. . . 4
β’ (π β π β π) |
9 | | pimdecfgtioc.d |
. . . 4
β’ πΌ = (-β(,]π) |
10 | 6, 7, 8, 9 | ressiocsup 44565 |
. . 3
β’ (π β π β πΌ) |
11 | 10, 4 | ssind 4231 |
. 2
β’ (π β π β (πΌ β© π΄)) |
12 | | pimdecfgtioc.x |
. . . 4
β’
β²π₯π |
13 | | elinel2 4195 |
. . . . . . . 8
β’ (π₯ β (πΌ β© π΄) β π₯ β π΄) |
14 | 13 | adantl 480 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π΄) |
15 | | pimdecfgtioc.r |
. . . . . . . . 9
β’ (π β π
β
β*) |
16 | 15 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
β
β*) |
17 | | pimdecfgtioc.f |
. . . . . . . . . 10
β’ (π β πΉ:π΄βΆβ*) |
18 | 3, 8 | sselid 3979 |
. . . . . . . . . 10
β’ (π β π β π΄) |
19 | 17, 18 | ffvelcdmd 7086 |
. . . . . . . . 9
β’ (π β (πΉβπ) β
β*) |
20 | 19 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ) β
β*) |
21 | 17 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β πΉ:π΄βΆβ*) |
22 | 21, 14 | ffvelcdmd 7086 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ₯) β
β*) |
23 | 8, 1 | eleqtrdi 2841 |
. . . . . . . . . . 11
β’ (π β π β {π₯ β π΄ β£ π
< (πΉβπ₯)}) |
24 | | nfrab1 3449 |
. . . . . . . . . . . . . . 15
β’
β²π₯{π₯ β π΄ β£ π
< (πΉβπ₯)} |
25 | 1, 24 | nfcxfr 2899 |
. . . . . . . . . . . . . 14
β’
β²π₯π |
26 | | nfcv 2901 |
. . . . . . . . . . . . . 14
β’
β²π₯β* |
27 | | nfcv 2901 |
. . . . . . . . . . . . . 14
β’
β²π₯
< |
28 | 25, 26, 27 | nfsup 9448 |
. . . . . . . . . . . . 13
β’
β²π₯sup(π, β*, <
) |
29 | 7, 28 | nfcxfr 2899 |
. . . . . . . . . . . 12
β’
β²π₯π |
30 | | nfcv 2901 |
. . . . . . . . . . . 12
β’
β²π₯π΄ |
31 | | nfcv 2901 |
. . . . . . . . . . . . 13
β’
β²π₯π
|
32 | | nfcv 2901 |
. . . . . . . . . . . . . 14
β’
β²π₯πΉ |
33 | 32, 29 | nffv 6900 |
. . . . . . . . . . . . 13
β’
β²π₯(πΉβπ) |
34 | 31, 27, 33 | nfbr 5194 |
. . . . . . . . . . . 12
β’
β²π₯ π
< (πΉβπ) |
35 | | fveq2 6890 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
36 | 35 | breq2d 5159 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π
< (πΉβπ₯) β π
< (πΉβπ))) |
37 | 29, 30, 34, 36 | elrabf 3678 |
. . . . . . . . . . 11
β’ (π β {π₯ β π΄ β£ π
< (πΉβπ₯)} β (π β π΄ β§ π
< (πΉβπ))) |
38 | 23, 37 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π β π΄ β§ π
< (πΉβπ))) |
39 | 38 | simprd 494 |
. . . . . . . . 9
β’ (π β π
< (πΉβπ)) |
40 | 39 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
< (πΉβπ)) |
41 | 18 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β π΄) |
42 | | pimdecfgtioc.i |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
43 | 42 | r19.21bi 3246 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
44 | 14, 43 | syldan 589 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
45 | 41, 44 | jca 510 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β (π β π΄ β§ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯)))) |
46 | | mnfxr 11275 |
. . . . . . . . . . 11
β’ -β
β β* |
47 | 46 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β -β β
β*) |
48 | | ressxr 11262 |
. . . . . . . . . . . 12
β’ β
β β* |
49 | 6, 8 | sseldd 3982 |
. . . . . . . . . . . 12
β’ (π β π β β) |
50 | 48, 49 | sselid 3979 |
. . . . . . . . . . 11
β’ (π β π β
β*) |
51 | 50 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β
β*) |
52 | | elinel1 4194 |
. . . . . . . . . . . 12
β’ (π₯ β (πΌ β© π΄) β π₯ β πΌ) |
53 | 52, 9 | eleqtrdi 2841 |
. . . . . . . . . . 11
β’ (π₯ β (πΌ β© π΄) β π₯ β (-β(,]π)) |
54 | 53 | adantl 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β (-β(,]π)) |
55 | | iocleub 44514 |
. . . . . . . . . 10
β’
((-β β β* β§ π β β* β§ π₯ β (-β(,]π)) β π₯ β€ π) |
56 | 47, 51, 54, 55 | syl3anc 1369 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β€ π) |
57 | | breq2 5151 |
. . . . . . . . . . 11
β’ (π¦ = π β (π₯ β€ π¦ β π₯ β€ π)) |
58 | | fveq2 6890 |
. . . . . . . . . . . 12
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
59 | 58 | breq1d 5157 |
. . . . . . . . . . 11
β’ (π¦ = π β ((πΉβπ¦) β€ (πΉβπ₯) β (πΉβπ) β€ (πΉβπ₯))) |
60 | 57, 59 | imbi12d 343 |
. . . . . . . . . 10
β’ (π¦ = π β ((π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯)) β (π₯ β€ π β (πΉβπ) β€ (πΉβπ₯)))) |
61 | 60 | rspcva 3609 |
. . . . . . . . 9
β’ ((π β π΄ β§ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) β (π₯ β€ π β (πΉβπ) β€ (πΉβπ₯))) |
62 | 45, 56, 61 | sylc 65 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ) β€ (πΉβπ₯)) |
63 | 16, 20, 22, 40, 62 | xrltletrd 13144 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
< (πΉβπ₯)) |
64 | 14, 63 | jca 510 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β© π΄)) β (π₯ β π΄ β§ π
< (πΉβπ₯))) |
65 | 1 | reqabi 3452 |
. . . . . 6
β’ (π₯ β π β (π₯ β π΄ β§ π
< (πΉβπ₯))) |
66 | 64, 65 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π) |
67 | 66 | ex 411 |
. . . 4
β’ (π β (π₯ β (πΌ β© π΄) β π₯ β π)) |
68 | 12, 67 | ralrimi 3252 |
. . 3
β’ (π β βπ₯ β (πΌ β© π΄)π₯ β π) |
69 | | nfv 1915 |
. . . . 5
β’
β²π₯ π§ β (πΌ β© π΄) |
70 | 69 | nfci 2884 |
. . . 4
β’
β²π₯(πΌ β© π΄) |
71 | 70, 25 | dfss3f 3972 |
. . 3
β’ ((πΌ β© π΄) β π β βπ₯ β (πΌ β© π΄)π₯ β π) |
72 | 68, 71 | sylibr 233 |
. 2
β’ (π β (πΌ β© π΄) β π) |
73 | 11, 72 | eqssd 3998 |
1
β’ (π β π = (πΌ β© π΄)) |