Step | Hyp | Ref
| Expression |
1 | | bndth.4 |
. . . . 5
β’ (π β πΉ β (π½ Cn πΎ)) |
2 | | bndth.1 |
. . . . . 6
β’ π = βͺ
π½ |
3 | | bndth.2 |
. . . . . . . 8
β’ πΎ = (topGenβran
(,)) |
4 | | retopon 24143 |
. . . . . . . 8
β’
(topGenβran (,)) β (TopOnββ) |
5 | 3, 4 | eqeltri 2830 |
. . . . . . 7
β’ πΎ β
(TopOnββ) |
6 | 5 | toponunii 22281 |
. . . . . 6
β’ β =
βͺ πΎ |
7 | 2, 6 | cnf 22613 |
. . . . 5
β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆβ) |
8 | 1, 7 | syl 17 |
. . . 4
β’ (π β πΉ:πβΆβ) |
9 | 8 | frnd 6677 |
. . 3
β’ (π β ran πΉ β β) |
10 | | unieq 4877 |
. . . . . . 7
β’ (π’ = ((,) β ({-β}
Γ β)) β βͺ π’ = βͺ ((,) β
({-β} Γ β))) |
11 | | imassrn 6025 |
. . . . . . . . . 10
β’ ((,)
β ({-β} Γ β)) β ran (,) |
12 | 11 | unissi 4875 |
. . . . . . . . 9
β’ βͺ ((,) β ({-β} Γ β)) β βͺ ran (,) |
13 | | unirnioo 13372 |
. . . . . . . . 9
β’ β =
βͺ ran (,) |
14 | 12, 13 | sseqtrri 3982 |
. . . . . . . 8
β’ βͺ ((,) β ({-β} Γ β)) β
β |
15 | | id 22 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯ β
β) |
16 | | ltp1 12000 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯ < (π₯ + 1)) |
17 | | ressxr 11204 |
. . . . . . . . . . . . 13
β’ β
β β* |
18 | | peano2re 11333 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π₯ + 1) β
β) |
19 | 17, 18 | sselid 3943 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯ + 1) β
β*) |
20 | | elioomnf 13367 |
. . . . . . . . . . . 12
β’ ((π₯ + 1) β β*
β (π₯ β
(-β(,)(π₯ + 1)) β
(π₯ β β β§
π₯ < (π₯ + 1)))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β β β (π₯ β (-β(,)(π₯ + 1)) β (π₯ β β β§ π₯ < (π₯ + 1)))) |
22 | 15, 16, 21 | mpbir2and 712 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β (-β(,)(π₯ + 1))) |
23 | | df-ov 7361 |
. . . . . . . . . . 11
β’
(-β(,)(π₯ + 1))
= ((,)ββ¨-β, (π₯ + 1)β©) |
24 | | mnfxr 11217 |
. . . . . . . . . . . . . . 15
β’ -β
β β* |
25 | 24 | elexi 3463 |
. . . . . . . . . . . . . 14
β’ -β
β V |
26 | 25 | snid 4623 |
. . . . . . . . . . . . 13
β’ -β
β {-β} |
27 | | opelxpi 5671 |
. . . . . . . . . . . . 13
β’
((-β β {-β} β§ (π₯ + 1) β β) β β¨-β,
(π₯ + 1)β© β
({-β} Γ β)) |
28 | 26, 18, 27 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π₯ β β β
β¨-β, (π₯ +
1)β© β ({-β} Γ β)) |
29 | | ioof 13370 |
. . . . . . . . . . . . . 14
β’
(,):(β* Γ β*)βΆπ«
β |
30 | | ffun 6672 |
. . . . . . . . . . . . . 14
β’
((,):(β* Γ β*)βΆπ«
β β Fun (,)) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ Fun
(,) |
32 | | snssi 4769 |
. . . . . . . . . . . . . . . 16
β’ (-β
β β* β {-β} β
β*) |
33 | 24, 32 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
{-β} β β* |
34 | | xpss12 5649 |
. . . . . . . . . . . . . . 15
β’
(({-β} β β* β§ β β
β*) β ({-β} Γ β) β
(β* Γ β*)) |
35 | 33, 17, 34 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
({-β} Γ β) β (β* Γ
β*) |
36 | 29 | fdmi 6681 |
. . . . . . . . . . . . . 14
β’ dom (,) =
(β* Γ β*) |
37 | 35, 36 | sseqtrri 3982 |
. . . . . . . . . . . . 13
β’
({-β} Γ β) β dom (,) |
38 | | funfvima2 7182 |
. . . . . . . . . . . . 13
β’ ((Fun (,)
β§ ({-β} Γ β) β dom (,)) β (β¨-β,
(π₯ + 1)β© β
({-β} Γ β) β ((,)ββ¨-β, (π₯ + 1)β©) β ((,) β
({-β} Γ β)))) |
39 | 31, 37, 38 | mp2an 691 |
. . . . . . . . . . . 12
β’
(β¨-β, (π₯
+ 1)β© β ({-β} Γ β) β
((,)ββ¨-β, (π₯ + 1)β©) β ((,) β ({-β}
Γ β))) |
40 | 28, 39 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β β β
((,)ββ¨-β, (π₯ + 1)β©) β ((,) β ({-β}
Γ β))) |
41 | 23, 40 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π₯ β β β
(-β(,)(π₯ + 1)) β
((,) β ({-β} Γ β))) |
42 | | elunii 4871 |
. . . . . . . . . 10
β’ ((π₯ β (-β(,)(π₯ + 1)) β§ (-β(,)(π₯ + 1)) β ((,) β
({-β} Γ β))) β π₯ β βͺ ((,)
β ({-β} Γ β))) |
43 | 22, 41, 42 | syl2anc 585 |
. . . . . . . . 9
β’ (π₯ β β β π₯ β βͺ ((,) β ({-β} Γ
β))) |
44 | 43 | ssriv 3949 |
. . . . . . . 8
β’ β
β βͺ ((,) β ({-β} Γ
β)) |
45 | 14, 44 | eqssi 3961 |
. . . . . . 7
β’ βͺ ((,) β ({-β} Γ β)) =
β |
46 | 10, 45 | eqtrdi 2789 |
. . . . . 6
β’ (π’ = ((,) β ({-β}
Γ β)) β βͺ π’ = β) |
47 | 46 | sseq2d 3977 |
. . . . 5
β’ (π’ = ((,) β ({-β}
Γ β)) β (ran πΉ β βͺ π’ β ran πΉ β β)) |
48 | | pweq 4575 |
. . . . . . 7
β’ (π’ = ((,) β ({-β}
Γ β)) β π« π’ = π« ((,) β ({-β} Γ
β))) |
49 | 48 | ineq1d 4172 |
. . . . . 6
β’ (π’ = ((,) β ({-β}
Γ β)) β (π« π’ β© Fin) = (π« ((,) β
({-β} Γ β)) β© Fin)) |
50 | 49 | rexeqdv 3313 |
. . . . 5
β’ (π’ = ((,) β ({-β}
Γ β)) β (βπ£ β (π« π’ β© Fin)ran πΉ β βͺ π£ β βπ£ β (π« ((,) β
({-β} Γ β)) β© Fin)ran πΉ β βͺ π£)) |
51 | 47, 50 | imbi12d 345 |
. . . 4
β’ (π’ = ((,) β ({-β}
Γ β)) β ((ran πΉ β βͺ π’ β βπ£ β (π« π’ β© Fin)ran πΉ β βͺ π£) β (ran πΉ β β β βπ£ β (π« ((,) β
({-β} Γ β)) β© Fin)ran πΉ β βͺ π£))) |
52 | | bndth.3 |
. . . . . 6
β’ (π β π½ β Comp) |
53 | | rncmp 22763 |
. . . . . 6
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β (πΎ βΎt ran πΉ) β Comp) |
54 | 52, 1, 53 | syl2anc 585 |
. . . . 5
β’ (π β (πΎ βΎt ran πΉ) β Comp) |
55 | | retop 24141 |
. . . . . . 7
β’
(topGenβran (,)) β Top |
56 | 3, 55 | eqeltri 2830 |
. . . . . 6
β’ πΎ β Top |
57 | 6 | cmpsub 22767 |
. . . . . 6
β’ ((πΎ β Top β§ ran πΉ β β) β ((πΎ βΎt ran πΉ) β Comp β
βπ’ β π«
πΎ(ran πΉ β βͺ π’ β βπ£ β (π« π’ β© Fin)ran πΉ β βͺ π£))) |
58 | 56, 9, 57 | sylancr 588 |
. . . . 5
β’ (π β ((πΎ βΎt ran πΉ) β Comp β βπ’ β π« πΎ(ran πΉ β βͺ π’ β βπ£ β (π« π’ β© Fin)ran πΉ β βͺ π£))) |
59 | 54, 58 | mpbid 231 |
. . . 4
β’ (π β βπ’ β π« πΎ(ran πΉ β βͺ π’ β βπ£ β (π« π’ β© Fin)ran πΉ β βͺ π£)) |
60 | | retopbas 24140 |
. . . . . . . . 9
β’ ran (,)
β TopBases |
61 | | bastg 22332 |
. . . . . . . . 9
β’ (ran (,)
β TopBases β ran (,) β (topGenβran (,))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . 8
β’ ran (,)
β (topGenβran (,)) |
63 | 62, 3 | sseqtrri 3982 |
. . . . . . 7
β’ ran (,)
β πΎ |
64 | 11, 63 | sstri 3954 |
. . . . . 6
β’ ((,)
β ({-β} Γ β)) β πΎ |
65 | 56, 64 | elpwi2 5304 |
. . . . 5
β’ ((,)
β ({-β} Γ β)) β π« πΎ |
66 | 65 | a1i 11 |
. . . 4
β’ (π β ((,) β ({-β}
Γ β)) β π« πΎ) |
67 | 51, 59, 66 | rspcdva 3581 |
. . 3
β’ (π β (ran πΉ β β β βπ£ β (π« ((,) β
({-β} Γ β)) β© Fin)ran πΉ β βͺ π£)) |
68 | 9, 67 | mpd 15 |
. 2
β’ (π β βπ£ β (π« ((,) β ({-β}
Γ β)) β© Fin)ran πΉ β βͺ π£) |
69 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) |
70 | | elin 3927 |
. . . . . . 7
β’ (π£ β (π« ((,) β
({-β} Γ β)) β© Fin) β (π£ β π« ((,) β ({-β}
Γ β)) β§ π£
β Fin)) |
71 | 69, 70 | sylib 217 |
. . . . . 6
β’ ((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β (π£ β π« ((,) β ({-β}
Γ β)) β§ π£
β Fin)) |
72 | 71 | adantrr 716 |
. . . . 5
β’ ((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β (π£ β π« ((,) β ({-β}
Γ β)) β§ π£
β Fin)) |
73 | 72 | simprd 497 |
. . . 4
β’ ((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β π£ β Fin) |
74 | 71 | simpld 496 |
. . . . . . 7
β’ ((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β π£ β π« ((,) β ({-β}
Γ β))) |
75 | 74 | elpwid 4570 |
. . . . . 6
β’ ((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β π£ β ((,) β ({-β} Γ
β))) |
76 | 33 | sseli 3941 |
. . . . . . . . . . . 12
β’ (π’ β {-β} β π’ β
β*) |
77 | 76 | adantr 482 |
. . . . . . . . . . 11
β’ ((π’ β {-β} β§ π€ β β) β π’ β
β*) |
78 | 17 | sseli 3941 |
. . . . . . . . . . . 12
β’ (π€ β β β π€ β
β*) |
79 | 78 | adantl 483 |
. . . . . . . . . . 11
β’ ((π’ β {-β} β§ π€ β β) β π€ β
β*) |
80 | | mnflt 13049 |
. . . . . . . . . . . . . . 15
β’ (π€ β β β -β
< π€) |
81 | | xrltnle 11227 |
. . . . . . . . . . . . . . . 16
β’
((-β β β* β§ π€ β β*) β (-β
< π€ β Β¬ π€ β€
-β)) |
82 | 24, 78, 81 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (π€ β β β (-β
< π€ β Β¬ π€ β€
-β)) |
83 | 80, 82 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π€ β β β Β¬
π€ β€
-β) |
84 | 83 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π’ β {-β} β§ π€ β β) β Β¬
π€ β€
-β) |
85 | | elsni 4604 |
. . . . . . . . . . . . . . 15
β’ (π’ β {-β} β π’ = -β) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π’ β {-β} β§ π€ β β) β π’ = -β) |
87 | 86 | breq2d 5118 |
. . . . . . . . . . . . 13
β’ ((π’ β {-β} β§ π€ β β) β (π€ β€ π’ β π€ β€ -β)) |
88 | 84, 87 | mtbird 325 |
. . . . . . . . . . . 12
β’ ((π’ β {-β} β§ π€ β β) β Β¬
π€ β€ π’) |
89 | | ioo0 13295 |
. . . . . . . . . . . . . 14
β’ ((π’ β β*
β§ π€ β
β*) β ((π’(,)π€) = β
β π€ β€ π’)) |
90 | 76, 78, 89 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π’ β {-β} β§ π€ β β) β ((π’(,)π€) = β
β π€ β€ π’)) |
91 | 90 | necon3abid 2977 |
. . . . . . . . . . . 12
β’ ((π’ β {-β} β§ π€ β β) β ((π’(,)π€) β β
β Β¬ π€ β€ π’)) |
92 | 88, 91 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π’ β {-β} β§ π€ β β) β (π’(,)π€) β β
) |
93 | | df-ioo 13274 |
. . . . . . . . . . . 12
β’ (,) =
(π¦ β
β*, π§
β β* β¦ {π£ β β* β£ (π¦ < π£ β§ π£ < π§)}) |
94 | | idd 24 |
. . . . . . . . . . . 12
β’ ((π₯ β β*
β§ π€ β
β*) β (π₯ < π€ β π₯ < π€)) |
95 | | xrltle 13074 |
. . . . . . . . . . . 12
β’ ((π₯ β β*
β§ π€ β
β*) β (π₯ < π€ β π₯ β€ π€)) |
96 | | idd 24 |
. . . . . . . . . . . 12
β’ ((π’ β β*
β§ π₯ β
β*) β (π’ < π₯ β π’ < π₯)) |
97 | | xrltle 13074 |
. . . . . . . . . . . 12
β’ ((π’ β β*
β§ π₯ β
β*) β (π’ < π₯ β π’ β€ π₯)) |
98 | 93, 94, 95, 96, 97 | ixxub 13291 |
. . . . . . . . . . 11
β’ ((π’ β β*
β§ π€ β
β* β§ (π’(,)π€) β β
) β sup((π’(,)π€), β*, < ) = π€) |
99 | 77, 79, 92, 98 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π’ β {-β} β§ π€ β β) β
sup((π’(,)π€), β*, < ) = π€) |
100 | | simpr 486 |
. . . . . . . . . 10
β’ ((π’ β {-β} β§ π€ β β) β π€ β
β) |
101 | 99, 100 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π’ β {-β} β§ π€ β β) β
sup((π’(,)π€), β*, < ) β
β) |
102 | 101 | rgen2 3191 |
. . . . . . . 8
β’
βπ’ β
{-β}βπ€ β
β sup((π’(,)π€), β*, < )
β β |
103 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π§ = β¨π’, π€β© β ((,)βπ§) = ((,)ββ¨π’, π€β©)) |
104 | | df-ov 7361 |
. . . . . . . . . . . 12
β’ (π’(,)π€) = ((,)ββ¨π’, π€β©) |
105 | 103, 104 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π§ = β¨π’, π€β© β ((,)βπ§) = (π’(,)π€)) |
106 | 105 | supeq1d 9387 |
. . . . . . . . . 10
β’ (π§ = β¨π’, π€β© β sup(((,)βπ§), β*, < ) =
sup((π’(,)π€), β*, <
)) |
107 | 106 | eleq1d 2819 |
. . . . . . . . 9
β’ (π§ = β¨π’, π€β© β (sup(((,)βπ§), β*, < )
β β β sup((π’(,)π€), β*, < ) β
β)) |
108 | 107 | ralxp 5798 |
. . . . . . . 8
β’
(βπ§ β
({-β} Γ β)sup(((,)βπ§), β*, < ) β β
β βπ’ β
{-β}βπ€ β
β sup((π’(,)π€), β*, < )
β β) |
109 | 102, 108 | mpbir 230 |
. . . . . . 7
β’
βπ§ β
({-β} Γ β)sup(((,)βπ§), β*, < ) β
β |
110 | | ffn 6669 |
. . . . . . . . 9
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
111 | 29, 110 | ax-mp 5 |
. . . . . . . 8
β’ (,) Fn
(β* Γ β*) |
112 | | supeq1 9386 |
. . . . . . . . . 10
β’ (π€ = ((,)βπ§) β sup(π€, β*, < ) =
sup(((,)βπ§),
β*, < )) |
113 | 112 | eleq1d 2819 |
. . . . . . . . 9
β’ (π€ = ((,)βπ§) β (sup(π€, β*, < ) β β
β sup(((,)βπ§),
β*, < ) β β)) |
114 | 113 | ralima 7189 |
. . . . . . . 8
β’ (((,) Fn
(β* Γ β*) β§ ({-β} Γ
β) β (β* Γ β*)) β
(βπ€ β ((,)
β ({-β} Γ β))sup(π€, β*, < ) β β
β βπ§ β
({-β} Γ β)sup(((,)βπ§), β*, < ) β
β)) |
115 | 111, 35, 114 | mp2an 691 |
. . . . . . 7
β’
(βπ€ β
((,) β ({-β} Γ β))sup(π€, β*, < ) β β
β βπ§ β
({-β} Γ β)sup(((,)βπ§), β*, < ) β
β) |
116 | 109, 115 | mpbir 230 |
. . . . . 6
β’
βπ€ β
((,) β ({-β} Γ β))sup(π€, β*, < ) β
β |
117 | | ssralv 4011 |
. . . . . 6
β’ (π£ β ((,) β
({-β} Γ β)) β (βπ€ β ((,) β ({-β} Γ
β))sup(π€,
β*, < ) β β β βπ€ β π£ sup(π€, β*, < ) β
β)) |
118 | 75, 116, 117 | mpisyl 21 |
. . . . 5
β’ ((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β βπ€ β π£ sup(π€, β*, < ) β
β) |
119 | 118 | adantrr 716 |
. . . 4
β’ ((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β βπ€ β π£ sup(π€, β*, < ) β
β) |
120 | | fimaxre3 12106 |
. . . 4
β’ ((π£ β Fin β§ βπ€ β π£ sup(π€, β*, < ) β β)
β βπ₯ β
β βπ€ β
π£ sup(π€, β*, < ) β€ π₯) |
121 | 73, 119, 120 | syl2anc 585 |
. . 3
β’ ((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β βπ₯ β β βπ€ β π£ sup(π€, β*, < ) β€ π₯) |
122 | | simplrr 777 |
. . . . . . . 8
β’ (((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β ran πΉ β βͺ π£) |
123 | 122 | sselda 3945 |
. . . . . . 7
β’ ((((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β§ π§ β ran πΉ) β π§ β βͺ π£) |
124 | | eluni2 4870 |
. . . . . . . 8
β’ (π§ β βͺ π£
β βπ€ β
π£ π§ β π€) |
125 | | r19.29r 3116 |
. . . . . . . . . 10
β’
((βπ€ β
π£ π§ β π€ β§ βπ€ β π£ sup(π€, β*, < ) β€ π₯) β βπ€ β π£ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) |
126 | | sspwuni 5061 |
. . . . . . . . . . . . . . . . . . 19
β’ (((,)
β ({-β} Γ β)) β π« β β βͺ ((,) β ({-β} Γ β)) β
β) |
127 | 14, 126 | mpbir 230 |
. . . . . . . . . . . . . . . . . 18
β’ ((,)
β ({-β} Γ β)) β π«
β |
128 | 75 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π£ β ((,) β ({-β} Γ
β))) |
129 | | simp2r 1201 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π€ β π£) |
130 | 128, 129 | sseldd 3946 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π€ β ((,) β ({-β} Γ
β))) |
131 | 127, 130 | sselid 3943 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π€ β π« β) |
132 | 131 | elpwid 4570 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π€ β β) |
133 | | simp3l 1202 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π§ β π€) |
134 | 132, 133 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π§ β β) |
135 | 118 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ π€ β π£) β sup(π€, β*, < ) β
β) |
136 | 135 | adantrl 715 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£)) β sup(π€, β*, < ) β
β) |
137 | 136 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β sup(π€, β*, < ) β
β) |
138 | | simp2l 1200 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π₯ β β) |
139 | 132, 17 | sstrdi 3957 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π€ β
β*) |
140 | | supxrub 13249 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β β*
β§ π§ β π€) β π§ β€ sup(π€, β*, <
)) |
141 | 139, 133,
140 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π§ β€ sup(π€, β*, <
)) |
142 | | simp3r 1203 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β sup(π€, β*, < ) β€ π₯) |
143 | 134, 137,
138, 141, 142 | letrd 11317 |
. . . . . . . . . . . . . 14
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£) β§ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯)) β π§ β€ π₯) |
144 | 143 | 3expia 1122 |
. . . . . . . . . . . . 13
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ (π₯ β β β§ π€ β π£)) β ((π§ β π€ β§ sup(π€, β*, < ) β€ π₯) β π§ β€ π₯)) |
145 | 144 | anassrs 469 |
. . . . . . . . . . . 12
β’ ((((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ π₯ β β) β§ π€ β π£) β ((π§ β π€ β§ sup(π€, β*, < ) β€ π₯) β π§ β€ π₯)) |
146 | 145 | rexlimdva 3149 |
. . . . . . . . . . 11
β’ (((π β§ π£ β (π« ((,) β ({-β}
Γ β)) β© Fin)) β§ π₯ β β) β (βπ€ β π£ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯) β π§ β€ π₯)) |
147 | 146 | adantlrr 720 |
. . . . . . . . . 10
β’ (((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β (βπ€ β π£ (π§ β π€ β§ sup(π€, β*, < ) β€ π₯) β π§ β€ π₯)) |
148 | 125, 147 | syl5 34 |
. . . . . . . . 9
β’ (((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β ((βπ€ β π£ π§ β π€ β§ βπ€ β π£ sup(π€, β*, < ) β€ π₯) β π§ β€ π₯)) |
149 | 148 | expdimp 454 |
. . . . . . . 8
β’ ((((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β§ βπ€ β π£ π§ β π€) β (βπ€ β π£ sup(π€, β*, < ) β€ π₯ β π§ β€ π₯)) |
150 | 124, 149 | sylan2b 595 |
. . . . . . 7
β’ ((((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β§ π§ β βͺ π£) β (βπ€ β π£ sup(π€, β*, < ) β€ π₯ β π§ β€ π₯)) |
151 | 123, 150 | syldan 592 |
. . . . . 6
β’ ((((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β§ π§ β ran πΉ) β (βπ€ β π£ sup(π€, β*, < ) β€ π₯ β π§ β€ π₯)) |
152 | 151 | ralrimdva 3148 |
. . . . 5
β’ (((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β (βπ€ β π£ sup(π€, β*, < ) β€ π₯ β βπ§ β ran πΉ π§ β€ π₯)) |
153 | 8 | ffnd 6670 |
. . . . . . 7
β’ (π β πΉ Fn π) |
154 | 153 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β πΉ Fn π) |
155 | | breq1 5109 |
. . . . . . 7
β’ (π§ = (πΉβπ¦) β (π§ β€ π₯ β (πΉβπ¦) β€ π₯)) |
156 | 155 | ralrn 7039 |
. . . . . 6
β’ (πΉ Fn π β (βπ§ β ran πΉ π§ β€ π₯ β βπ¦ β π (πΉβπ¦) β€ π₯)) |
157 | 154, 156 | syl 17 |
. . . . 5
β’ (((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β (βπ§ β ran πΉ π§ β€ π₯ β βπ¦ β π (πΉβπ¦) β€ π₯)) |
158 | 152, 157 | sylibd 238 |
. . . 4
β’ (((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β§ π₯ β β) β (βπ€ β π£ sup(π€, β*, < ) β€ π₯ β βπ¦ β π (πΉβπ¦) β€ π₯)) |
159 | 158 | reximdva 3162 |
. . 3
β’ ((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β (βπ₯ β β βπ€ β π£ sup(π€, β*, < ) β€ π₯ β βπ₯ β β βπ¦ β π (πΉβπ¦) β€ π₯)) |
160 | 121, 159 | mpd 15 |
. 2
β’ ((π β§ (π£ β (π« ((,) β ({-β}
Γ β)) β© Fin) β§ ran πΉ β βͺ π£)) β βπ₯ β β βπ¦ β π (πΉβπ¦) β€ π₯) |
161 | 68, 160 | rexlimddv 3155 |
1
β’ (π β βπ₯ β β βπ¦ β π (πΉβπ¦) β€ π₯) |