Step | Hyp | Ref
| Expression |
1 | | icoopn.k |
. . . . 5
β’ πΎ = (topGenβran
(,)) |
2 | | retop 24128 |
. . . . 5
β’
(topGenβran (,)) β Top |
3 | 1, 2 | eqeltri 2834 |
. . . 4
β’ πΎ β Top |
4 | 3 | a1i 11 |
. . 3
β’ (π β πΎ β Top) |
5 | | ovexd 7393 |
. . 3
β’ (π β (π΄[,)π΅) β V) |
6 | | iooretop 24132 |
. . . . 5
β’
(-β(,)πΆ)
β (topGenβran (,)) |
7 | 6, 1 | eleqtrri 2837 |
. . . 4
β’
(-β(,)πΆ)
β πΎ |
8 | 7 | a1i 11 |
. . 3
β’ (π β (-β(,)πΆ) β πΎ) |
9 | | elrestr 17311 |
. . 3
β’ ((πΎ β Top β§ (π΄[,)π΅) β V β§ (-β(,)πΆ) β πΎ) β ((-β(,)πΆ) β© (π΄[,)π΅)) β (πΎ βΎt (π΄[,)π΅))) |
10 | 4, 5, 8, 9 | syl3anc 1372 |
. 2
β’ (π β ((-β(,)πΆ) β© (π΄[,)π΅)) β (πΎ βΎt (π΄[,)π΅))) |
11 | | icoopn.a |
. . . . . . 7
β’ (π β π΄ β β) |
12 | 11 | rexrd 11206 |
. . . . . 6
β’ (π β π΄ β
β*) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π΄ β
β*) |
14 | | icoopn.c |
. . . . . 6
β’ (π β πΆ β
β*) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β πΆ β
β*) |
16 | | elinel1 4156 |
. . . . . . . 8
β’ (π₯ β ((-β(,)πΆ) β© (π΄[,)π΅)) β π₯ β (-β(,)πΆ)) |
17 | | elioore 13295 |
. . . . . . . 8
β’ (π₯ β (-β(,)πΆ) β π₯ β β) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ (π₯ β ((-β(,)πΆ) β© (π΄[,)π΅)) β π₯ β β) |
19 | 18 | rexrd 11206 |
. . . . . 6
β’ (π₯ β ((-β(,)πΆ) β© (π΄[,)π΅)) β π₯ β β*) |
20 | 19 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π₯ β β*) |
21 | | icoopn.b |
. . . . . . 7
β’ (π β π΅ β
β*) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π΅ β
β*) |
23 | | elinel2 4157 |
. . . . . . 7
β’ (π₯ β ((-β(,)πΆ) β© (π΄[,)π΅)) β π₯ β (π΄[,)π΅)) |
24 | 23 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π₯ β (π΄[,)π΅)) |
25 | | icogelb 13316 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,)π΅)) β π΄ β€ π₯) |
26 | 13, 22, 24, 25 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π΄ β€ π₯) |
27 | | mnfxr 11213 |
. . . . . . 7
β’ -β
β β* |
28 | 27 | a1i 11 |
. . . . . 6
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β -β β
β*) |
29 | 16 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π₯ β (-β(,)πΆ)) |
30 | | iooltub 43755 |
. . . . . 6
β’
((-β β β* β§ πΆ β β* β§ π₯ β (-β(,)πΆ)) β π₯ < πΆ) |
31 | 28, 15, 29, 30 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π₯ < πΆ) |
32 | 13, 15, 20, 26, 31 | elicod 13315 |
. . . 4
β’ ((π β§ π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) β π₯ β (π΄[,)πΆ)) |
33 | 27 | a1i 11 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β -β β
β*) |
34 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β πΆ β
β*) |
35 | | icossre 13346 |
. . . . . . . 8
β’ ((π΄ β β β§ πΆ β β*)
β (π΄[,)πΆ) β
β) |
36 | 11, 14, 35 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΄[,)πΆ) β β) |
37 | 36 | sselda 3945 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ β β) |
38 | 37 | mnfltd 13046 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β -β < π₯) |
39 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π΄ β
β*) |
40 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ β (π΄[,)πΆ)) |
41 | | icoltub 43753 |
. . . . . . 7
β’ ((π΄ β β*
β§ πΆ β
β* β§ π₯
β (π΄[,)πΆ)) β π₯ < πΆ) |
42 | 39, 34, 40, 41 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ < πΆ) |
43 | 33, 34, 37, 38, 42 | eliood 43743 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ β (-β(,)πΆ)) |
44 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π΅ β
β*) |
45 | 37 | rexrd 11206 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ β β*) |
46 | | icogelb 13316 |
. . . . . . 7
β’ ((π΄ β β*
β§ πΆ β
β* β§ π₯
β (π΄[,)πΆ)) β π΄ β€ π₯) |
47 | 39, 34, 40, 46 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π΄ β€ π₯) |
48 | | icoopn.cleb |
. . . . . . . 8
β’ (π β πΆ β€ π΅) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,)πΆ)) β πΆ β€ π΅) |
50 | 45, 34, 44, 42, 49 | xrltletrd 13081 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ < π΅) |
51 | 39, 44, 45, 47, 50 | elicod 13315 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ β (π΄[,)π΅)) |
52 | 43, 51 | elind 4155 |
. . . 4
β’ ((π β§ π₯ β (π΄[,)πΆ)) β π₯ β ((-β(,)πΆ) β© (π΄[,)π΅))) |
53 | 32, 52 | impbida 800 |
. . 3
β’ (π β (π₯ β ((-β(,)πΆ) β© (π΄[,)π΅)) β π₯ β (π΄[,)πΆ))) |
54 | 53 | eqrdv 2735 |
. 2
β’ (π β ((-β(,)πΆ) β© (π΄[,)π΅)) = (π΄[,)πΆ)) |
55 | | icoopn.j |
. . . 4
β’ π½ = (πΎ βΎt (π΄[,)π΅)) |
56 | 55 | eqcomi 2746 |
. . 3
β’ (πΎ βΎt (π΄[,)π΅)) = π½ |
57 | 56 | a1i 11 |
. 2
β’ (π β (πΎ βΎt (π΄[,)π΅)) = π½) |
58 | 10, 54, 57 | 3eltr3d 2852 |
1
β’ (π β (π΄[,)πΆ) β π½) |