Step | Hyp | Ref
| Expression |
1 | | pimdecfgtioc.y |
. . . . . . 7
β’ π = {π₯ β π΄ β£ π
< (πΉβπ₯)} |
2 | | ssrab2 4078 |
. . . . . . 7
β’ {π₯ β π΄ β£ π
< (πΉβπ₯)} β π΄ |
3 | 1, 2 | eqsstri 4017 |
. . . . . 6
β’ π β π΄ |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β π β π΄) |
5 | | pimdecfgtioc.a |
. . . . 5
β’ (π β π΄ β β) |
6 | 4, 5 | sstrd 3993 |
. . . 4
β’ (π β π β β) |
7 | | pimdecfgtioc.c |
. . . 4
β’ π = sup(π, β*, <
) |
8 | | pimdecfgtioc.e |
. . . 4
β’ (π β π β π) |
9 | | pimdecfgtioc.d |
. . . 4
β’ πΌ = (-β(,]π) |
10 | 6, 7, 8, 9 | ressiocsup 44267 |
. . 3
β’ (π β π β πΌ) |
11 | 10, 4 | ssind 4233 |
. 2
β’ (π β π β (πΌ β© π΄)) |
12 | | pimdecfgtioc.x |
. . . 4
β’
β²π₯π |
13 | | elinel2 4197 |
. . . . . . . 8
β’ (π₯ β (πΌ β© π΄) β π₯ β π΄) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π΄) |
15 | | pimdecfgtioc.r |
. . . . . . . . 9
β’ (π β π
β
β*) |
16 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
β
β*) |
17 | | pimdecfgtioc.f |
. . . . . . . . . 10
β’ (π β πΉ:π΄βΆβ*) |
18 | 3, 8 | sselid 3981 |
. . . . . . . . . 10
β’ (π β π β π΄) |
19 | 17, 18 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ (π β (πΉβπ) β
β*) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ) β
β*) |
21 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β πΉ:π΄βΆβ*) |
22 | 21, 14 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ₯) β
β*) |
23 | 8, 1 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (π β π β {π₯ β π΄ β£ π
< (πΉβπ₯)}) |
24 | | nfrab1 3452 |
. . . . . . . . . . . . . . 15
β’
β²π₯{π₯ β π΄ β£ π
< (πΉβπ₯)} |
25 | 1, 24 | nfcxfr 2902 |
. . . . . . . . . . . . . 14
β’
β²π₯π |
26 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯β* |
27 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯
< |
28 | 25, 26, 27 | nfsup 9446 |
. . . . . . . . . . . . 13
β’
β²π₯sup(π, β*, <
) |
29 | 7, 28 | nfcxfr 2902 |
. . . . . . . . . . . 12
β’
β²π₯π |
30 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π₯π΄ |
31 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯π
|
32 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯πΉ |
33 | 32, 29 | nffv 6902 |
. . . . . . . . . . . . 13
β’
β²π₯(πΉβπ) |
34 | 31, 27, 33 | nfbr 5196 |
. . . . . . . . . . . 12
β’
β²π₯ π
< (πΉβπ) |
35 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
36 | 35 | breq2d 5161 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π
< (πΉβπ₯) β π
< (πΉβπ))) |
37 | 29, 30, 34, 36 | elrabf 3680 |
. . . . . . . . . . 11
β’ (π β {π₯ β π΄ β£ π
< (πΉβπ₯)} β (π β π΄ β§ π
< (πΉβπ))) |
38 | 23, 37 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π β π΄ β§ π
< (πΉβπ))) |
39 | 38 | simprd 497 |
. . . . . . . . 9
β’ (π β π
< (πΉβπ)) |
40 | 39 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
< (πΉβπ)) |
41 | 18 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β π΄) |
42 | | pimdecfgtioc.i |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
43 | 42 | r19.21bi 3249 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
44 | 14, 43 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) |
45 | 41, 44 | jca 513 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β (π β π΄ β§ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯)))) |
46 | | mnfxr 11271 |
. . . . . . . . . . 11
β’ -β
β β* |
47 | 46 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β -β β
β*) |
48 | | ressxr 11258 |
. . . . . . . . . . . 12
β’ β
β β* |
49 | 6, 8 | sseldd 3984 |
. . . . . . . . . . . 12
β’ (π β π β β) |
50 | 48, 49 | sselid 3981 |
. . . . . . . . . . 11
β’ (π β π β
β*) |
51 | 50 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π β
β*) |
52 | | elinel1 4196 |
. . . . . . . . . . . 12
β’ (π₯ β (πΌ β© π΄) β π₯ β πΌ) |
53 | 52, 9 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (π₯ β (πΌ β© π΄) β π₯ β (-β(,]π)) |
54 | 53 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β (-β(,]π)) |
55 | | iocleub 44216 |
. . . . . . . . . 10
β’
((-β β β* β§ π β β* β§ π₯ β (-β(,]π)) β π₯ β€ π) |
56 | 47, 51, 54, 55 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β€ π) |
57 | | breq2 5153 |
. . . . . . . . . . 11
β’ (π¦ = π β (π₯ β€ π¦ β π₯ β€ π)) |
58 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
59 | 58 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π¦ = π β ((πΉβπ¦) β€ (πΉβπ₯) β (πΉβπ) β€ (πΉβπ₯))) |
60 | 57, 59 | imbi12d 345 |
. . . . . . . . . 10
β’ (π¦ = π β ((π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯)) β (π₯ β€ π β (πΉβπ) β€ (πΉβπ₯)))) |
61 | 60 | rspcva 3611 |
. . . . . . . . 9
β’ ((π β π΄ β§ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) β (π₯ β€ π β (πΉβπ) β€ (πΉβπ₯))) |
62 | 45, 56, 61 | sylc 65 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β© π΄)) β (πΉβπ) β€ (πΉβπ₯)) |
63 | 16, 20, 22, 40, 62 | xrltletrd 13140 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β© π΄)) β π
< (πΉβπ₯)) |
64 | 14, 63 | jca 513 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β© π΄)) β (π₯ β π΄ β§ π
< (πΉβπ₯))) |
65 | 1 | reqabi 3455 |
. . . . . 6
β’ (π₯ β π β (π₯ β π΄ β§ π
< (πΉβπ₯))) |
66 | 64, 65 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β© π΄)) β π₯ β π) |
67 | 66 | ex 414 |
. . . 4
β’ (π β (π₯ β (πΌ β© π΄) β π₯ β π)) |
68 | 12, 67 | ralrimi 3255 |
. . 3
β’ (π β βπ₯ β (πΌ β© π΄)π₯ β π) |
69 | | nfv 1918 |
. . . . 5
β’
β²π₯ π§ β (πΌ β© π΄) |
70 | 69 | nfci 2887 |
. . . 4
β’
β²π₯(πΌ β© π΄) |
71 | 70, 25 | dfss3f 3974 |
. . 3
β’ ((πΌ β© π΄) β π β βπ₯ β (πΌ β© π΄)π₯ β π) |
72 | 68, 71 | sylibr 233 |
. 2
β’ (π β (πΌ β© π΄) β π) |
73 | 11, 72 | eqssd 4000 |
1
β’ (π β π = (πΌ β© π΄)) |