Step | Hyp | Ref
| Expression |
1 | | stoweidlem57.2 |
. . . . . . . . . 10
β’
β²π‘π |
2 | | stoweidlem57.3 |
. . . . . . . . . . 11
β’
β²π‘π |
3 | | stoweidlem57.1 |
. . . . . . . . . . . 12
β’
β²π‘π· |
4 | 3 | nfcri 2891 |
. . . . . . . . . . 11
β’
β²π‘ π β π· |
5 | 2, 4 | nfan 1903 |
. . . . . . . . . 10
β’
β²π‘(π β§ π β π·) |
6 | | stoweidlem57.6 |
. . . . . . . . . 10
β’ πΎ = (topGenβran
(,)) |
7 | | stoweidlem57.10 |
. . . . . . . . . . 11
β’ (π β π½ β Comp) |
8 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π½ β Comp) |
9 | | stoweidlem57.7 |
. . . . . . . . . 10
β’ π = βͺ
π½ |
10 | | stoweidlem57.8 |
. . . . . . . . . 10
β’ πΆ = (π½ Cn πΎ) |
11 | | stoweidlem57.11 |
. . . . . . . . . . 11
β’ (π β π΄ β πΆ) |
12 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π΄ β πΆ) |
13 | | stoweidlem57.12 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
14 | 13 | 3adant1r 1178 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
15 | | stoweidlem57.13 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
16 | 15 | 3adant1r 1178 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
17 | | stoweidlem57.14 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) |
18 | 17 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β β) β (π‘ β π β¦ π) β π΄) |
19 | | stoweidlem57.15 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
20 | 19 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
21 | | stoweidlem57.9 |
. . . . . . . . . . . 12
β’ π = (π β π΅) |
22 | | stoweidlem57.16 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β (Clsdβπ½)) |
23 | | cmptop 22762 |
. . . . . . . . . . . . . . 15
β’ (π½ β Comp β π½ β Top) |
24 | 9 | iscld 22394 |
. . . . . . . . . . . . . . 15
β’ (π½ β Top β (π΅ β (Clsdβπ½) β (π΅ β π β§ (π β π΅) β π½))) |
25 | 7, 23, 24 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ β (Clsdβπ½) β (π΅ β π β§ (π β π΅) β π½))) |
26 | 22, 25 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β π β§ (π β π΅) β π½)) |
27 | 26 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β (π β π΅) β π½) |
28 | 21, 27 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β π β π½) |
29 | 28 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π β π½) |
30 | | stoweidlem57.17 |
. . . . . . . . . . . . . 14
β’ (π β π· β (Clsdβπ½)) |
31 | 9 | cldss 22396 |
. . . . . . . . . . . . . 14
β’ (π· β (Clsdβπ½) β π· β π) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π· β π) |
33 | 32 | sselda 3945 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β π β π) |
34 | | stoweidlem57.18 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ β© π·) = β
) |
35 | | disjr 4410 |
. . . . . . . . . . . . . 14
β’ ((π΅ β© π·) = β
β βπ β π· Β¬ π β π΅) |
36 | 34, 35 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β βπ β π· Β¬ π β π΅) |
37 | 36 | r19.21bi 3233 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β Β¬ π β π΅) |
38 | 33, 37 | eldifd 3922 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π β (π β π΅)) |
39 | 38, 21 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π β π) |
40 | 1, 5, 6, 8, 9, 10,
12, 14, 16, 18, 20, 29, 39 | stoweidlem56 44383 |
. . . . . . . . 9
β’ ((π β§ π β π·) β βπ€ β π½ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) |
41 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β π€ β π½) |
42 | | simprll 778 |
. . . . . . . . . . 11
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β π β π€) |
43 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))) |
44 | | stoweidlem57.5 |
. . . . . . . . . . . . 13
β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
45 | 44 | reqabi 3428 |
. . . . . . . . . . . 12
β’ (π€ β π β (π€ β π½ β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) |
46 | 41, 43, 45 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β π€ β π) |
47 | 41, 42, 46 | jca32 517 |
. . . . . . . . . 10
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β (π€ β π½ β§ (π β π€ β§ π€ β π))) |
48 | 47 | reximi2 3079 |
. . . . . . . . 9
β’
(βπ€ β
π½ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))) β βπ€ β π½ (π β π€ β§ π€ β π)) |
49 | | rexex 3076 |
. . . . . . . . 9
β’
(βπ€ β
π½ (π β π€ β§ π€ β π) β βπ€(π β π€ β§ π€ β π)) |
50 | 40, 48, 49 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π β π·) β βπ€(π β π€ β§ π€ β π)) |
51 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π€π |
52 | | nfrab1 3425 |
. . . . . . . . . 10
β’
β²π€{π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
53 | 44, 52 | nfcxfr 2902 |
. . . . . . . . 9
β’
β²π€π |
54 | 51, 53 | elunif 43309 |
. . . . . . . 8
β’ (π β βͺ π
β βπ€(π β π€ β§ π€ β π)) |
55 | 50, 54 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β π·) β π β βͺ π) |
56 | 55 | ex 414 |
. . . . . 6
β’ (π β (π β π· β π β βͺ π)) |
57 | 56 | ssrdv 3951 |
. . . . 5
β’ (π β π· β βͺ π) |
58 | | cmpcld 22769 |
. . . . . . . 8
β’ ((π½ β Comp β§ π· β (Clsdβπ½)) β (π½ βΎt π·) β Comp) |
59 | 7, 30, 58 | syl2anc 585 |
. . . . . . 7
β’ (π β (π½ βΎt π·) β Comp) |
60 | 7, 23 | syl 17 |
. . . . . . . 8
β’ (π β π½ β Top) |
61 | 9 | cmpsub 22767 |
. . . . . . . 8
β’ ((π½ β Top β§ π· β π) β ((π½ βΎt π·) β Comp β βπ β π« π½(π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’))) |
62 | 60, 32, 61 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π½ βΎt π·) β Comp β βπ β π« π½(π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’))) |
63 | 59, 62 | mpbid 231 |
. . . . . 6
β’ (π β βπ β π« π½(π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’)) |
64 | | ssrab2 4038 |
. . . . . . . 8
β’ {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} β π½ |
65 | 44, 64 | eqsstri 3979 |
. . . . . . 7
β’ π β π½ |
66 | 44, 7 | rabexd 5291 |
. . . . . . . 8
β’ (π β π β V) |
67 | | elpwg 4564 |
. . . . . . . 8
β’ (π β V β (π β π« π½ β π β π½)) |
68 | 66, 67 | syl 17 |
. . . . . . 7
β’ (π β (π β π« π½ β π β π½)) |
69 | 65, 68 | mpbiri 258 |
. . . . . 6
β’ (π β π β π« π½) |
70 | | unieq 4877 |
. . . . . . . . 9
β’ (π = π β βͺ π = βͺ
π) |
71 | 70 | sseq2d 3977 |
. . . . . . . 8
β’ (π = π β (π· β βͺ π β π· β βͺ π)) |
72 | | pweq 4575 |
. . . . . . . . . 10
β’ (π = π β π« π = π« π) |
73 | 72 | ineq1d 4172 |
. . . . . . . . 9
β’ (π = π β (π« π β© Fin) = (π« π β© Fin)) |
74 | 73 | rexeqdv 3313 |
. . . . . . . 8
β’ (π = π β (βπ’ β (π« π β© Fin)π· β βͺ π’ β βπ’ β (π« π β© Fin)π· β βͺ π’)) |
75 | 71, 74 | imbi12d 345 |
. . . . . . 7
β’ (π = π β ((π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’) β (π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’))) |
76 | 75 | rspccva 3579 |
. . . . . 6
β’
((βπ β
π« π½(π· β βͺ π
β βπ’ β
(π« π β©
Fin)π· β βͺ π’)
β§ π β π«
π½) β (π· β βͺ π
β βπ’ β
(π« π β©
Fin)π· β βͺ π’)) |
77 | 63, 69, 76 | syl2anc 585 |
. . . . 5
β’ (π β (π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’)) |
78 | 57, 77 | mpd 15 |
. . . 4
β’ (π β βπ’ β (π« π β© Fin)π· β βͺ π’) |
79 | | elinel1 4156 |
. . . . . . . . 9
β’ (π’ β (π« π β© Fin) β π’ β π« π) |
80 | | elpwi 4568 |
. . . . . . . . . . 11
β’ (π’ β π« π β π’ β π) |
81 | 80 | ssdifssd 4103 |
. . . . . . . . . 10
β’ (π’ β π« π β (π’ β {β
}) β π) |
82 | | vex 3448 |
. . . . . . . . . . . 12
β’ π’ β V |
83 | | difexg 5285 |
. . . . . . . . . . . 12
β’ (π’ β V β (π’ β {β
}) β
V) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π’ β {β
}) β
V |
85 | 84 | elpw 4565 |
. . . . . . . . . 10
β’ ((π’ β {β
}) β
π« π β (π’ β {β
}) β
π) |
86 | 81, 85 | sylibr 233 |
. . . . . . . . 9
β’ (π’ β π« π β (π’ β {β
}) β π« π) |
87 | 79, 86 | syl 17 |
. . . . . . . 8
β’ (π’ β (π« π β© Fin) β (π’ β {β
}) β
π« π) |
88 | | elinel2 4157 |
. . . . . . . . 9
β’ (π’ β (π« π β© Fin) β π’ β Fin) |
89 | | diffi 9126 |
. . . . . . . . 9
β’ (π’ β Fin β (π’ β {β
}) β
Fin) |
90 | 88, 89 | syl 17 |
. . . . . . . 8
β’ (π’ β (π« π β© Fin) β (π’ β {β
}) β
Fin) |
91 | 87, 90 | elind 4155 |
. . . . . . 7
β’ (π’ β (π« π β© Fin) β (π’ β {β
}) β
(π« π β©
Fin)) |
92 | 91 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β (π’ β {β
}) β (π« π β© Fin)) |
93 | | unidif0 5316 |
. . . . . . . . 9
β’ βͺ (π’
β {β
}) = βͺ π’ |
94 | 93 | sseq2i 3974 |
. . . . . . . 8
β’ (π· β βͺ (π’
β {β
}) β π·
β βͺ π’) |
95 | 94 | biimpri 227 |
. . . . . . 7
β’ (π· β βͺ π’
β π· β βͺ (π’
β {β
})) |
96 | 95 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β π· β βͺ (π’ β
{β
})) |
97 | | eldifsni 4751 |
. . . . . . . 8
β’ (π€ β (π’ β {β
}) β π€ β β
) |
98 | 97 | rgen 3063 |
. . . . . . 7
β’
βπ€ β
(π’ β {β
})π€ β β
|
99 | 98 | a1i 11 |
. . . . . 6
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β βπ€ β (π’ β {β
})π€ β β
) |
100 | | unieq 4877 |
. . . . . . . . 9
β’ (π = (π’ β {β
}) β βͺ π =
βͺ (π’ β {β
})) |
101 | 100 | sseq2d 3977 |
. . . . . . . 8
β’ (π = (π’ β {β
}) β (π· β βͺ π β π· β βͺ (π’ β
{β
}))) |
102 | | raleq 3308 |
. . . . . . . 8
β’ (π = (π’ β {β
}) β (βπ€ β π π€ β β
β βπ€ β (π’ β {β
})π€ β β
)) |
103 | 101, 102 | anbi12d 632 |
. . . . . . 7
β’ (π = (π’ β {β
}) β ((π· β βͺ π
β§ βπ€ β
π π€ β β
) β (π· β βͺ (π’ β {β
}) β§
βπ€ β (π’ β {β
})π€ β
β
))) |
104 | 103 | rspcev 3580 |
. . . . . 6
β’ (((π’ β {β
}) β
(π« π β© Fin)
β§ (π· β βͺ (π’
β {β
}) β§ βπ€ β (π’ β {β
})π€ β β
)) β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
)) |
105 | 92, 96, 99, 104 | syl12anc 836 |
. . . . 5
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
)) |
106 | 105 | rexlimdv3a 3153 |
. . . 4
β’ (π β (βπ’ β (π« π β© Fin)π· β βͺ π’ β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
))) |
107 | 78, 106 | mpd 15 |
. . 3
β’ (π β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
)) |
108 | | nfv 1918 |
. . . . . 6
β’
β²βπ |
109 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ββ+ |
110 | | nfre1 3267 |
. . . . . . . . . . . 12
β’
β²βββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
111 | 109, 110 | nfralw 3293 |
. . . . . . . . . . 11
β’
β²ββπ β β+
ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
112 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²βπ½ |
113 | 111, 112 | nfrabw 3439 |
. . . . . . . . . 10
β’
β²β{π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
114 | 44, 113 | nfcxfr 2902 |
. . . . . . . . 9
β’
β²βπ |
115 | 114 | nfpw 4580 |
. . . . . . . 8
β’
β²βπ« π |
116 | | nfcv 2904 |
. . . . . . . 8
β’
β²βFin |
117 | 115, 116 | nfin 4177 |
. . . . . . 7
β’
β²β(π« π β© Fin) |
118 | 117 | nfcri 2891 |
. . . . . 6
β’
β²β π β (π« π β© Fin) |
119 | | nfv 1918 |
. . . . . 6
β’
β²β(π· β βͺ π
β§ βπ€ β
π π€ β β
) |
120 | 108, 118,
119 | nf3an 1905 |
. . . . 5
β’
β²β(π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) |
121 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π‘β+ |
122 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π‘π΄ |
123 | | nfra1 3266 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
124 | | nfra1 3266 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β π€ (ββπ‘) < π |
125 | | nfra1 3266 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β (π β π)(1 β π) < (ββπ‘) |
126 | 123, 124,
125 | nf3an 1905 |
. . . . . . . . . . . . 13
β’
β²π‘(βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
127 | 122, 126 | nfrexw 3295 |
. . . . . . . . . . . 12
β’
β²π‘ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
128 | 121, 127 | nfralw 3293 |
. . . . . . . . . . 11
β’
β²π‘βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
129 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π‘π½ |
130 | 128, 129 | nfrabw 3439 |
. . . . . . . . . 10
β’
β²π‘{π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
131 | 44, 130 | nfcxfr 2902 |
. . . . . . . . 9
β’
β²π‘π |
132 | 131 | nfpw 4580 |
. . . . . . . 8
β’
β²π‘π« π |
133 | | nfcv 2904 |
. . . . . . . 8
β’
β²π‘Fin |
134 | 132, 133 | nfin 4177 |
. . . . . . 7
β’
β²π‘(π« π β© Fin) |
135 | 134 | nfcri 2891 |
. . . . . 6
β’
β²π‘ π β (π« π β© Fin) |
136 | | nfcv 2904 |
. . . . . . . 8
β’
β²π‘βͺ π |
137 | 3, 136 | nfss 3937 |
. . . . . . 7
β’
β²π‘ π· β βͺ π |
138 | | nfv 1918 |
. . . . . . 7
β’
β²π‘βπ€ β π π€ β β
|
139 | 137, 138 | nfan 1903 |
. . . . . 6
β’
β²π‘(π· β βͺ π
β§ βπ€ β
π π€ β β
) |
140 | 2, 135, 139 | nf3an 1905 |
. . . . 5
β’
β²π‘(π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) |
141 | | nfv 1918 |
. . . . . 6
β’
β²π€π |
142 | 53 | nfpw 4580 |
. . . . . . . 8
β’
β²π€π« π |
143 | | nfcv 2904 |
. . . . . . . 8
β’
β²π€Fin |
144 | 142, 143 | nfin 4177 |
. . . . . . 7
β’
β²π€(π« π β© Fin) |
145 | 144 | nfcri 2891 |
. . . . . 6
β’
β²π€ π β (π« π β© Fin) |
146 | | nfv 1918 |
. . . . . . 7
β’
β²π€ π· β βͺ π |
147 | | nfra1 3266 |
. . . . . . 7
β’
β²π€βπ€ β π π€ β β
|
148 | 146, 147 | nfan 1903 |
. . . . . 6
β’
β²π€(π· β βͺ π
β§ βπ€ β
π π€ β β
) |
149 | 141, 145,
148 | nf3an 1905 |
. . . . 5
β’
β²π€(π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) |
150 | | stoweidlem57.4 |
. . . . 5
β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
151 | | simp2 1138 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π β (π« π β© Fin)) |
152 | | simp3l 1202 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π· β βͺ π) |
153 | | stoweidlem57.19 |
. . . . . 6
β’ (π β π· β β
) |
154 | 153 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π· β β
) |
155 | | stoweidlem57.20 |
. . . . . 6
β’ (π β πΈ β
β+) |
156 | 155 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β πΈ β
β+) |
157 | 26 | simpld 496 |
. . . . . 6
β’ (π β π΅ β π) |
158 | 157 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π΅ β π) |
159 | 66 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π β V) |
160 | | retop 24141 |
. . . . . . . . 9
β’
(topGenβran (,)) β Top |
161 | 6, 160 | eqeltri 2830 |
. . . . . . . 8
β’ πΎ β Top |
162 | | cnfex 43321 |
. . . . . . . 8
β’ ((π½ β Top β§ πΎ β Top) β (π½ Cn πΎ) β V) |
163 | 60, 161, 162 | sylancl 587 |
. . . . . . 7
β’ (π β (π½ Cn πΎ) β V) |
164 | 11, 10 | sseqtrdi 3995 |
. . . . . . 7
β’ (π β π΄ β (π½ Cn πΎ)) |
165 | 163, 164 | ssexd 5282 |
. . . . . 6
β’ (π β π΄ β V) |
166 | 165 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π΄ β V) |
167 | 120, 140,
149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166 | stoweidlem39 44366 |
. . . 4
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
168 | 167 | rexlimdv3a 3153 |
. . 3
β’ (π β (βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
) β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))))) |
169 | 107, 168 | mpd 15 |
. 2
β’ (π β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
170 | | nfv 1918 |
. . . . . . 7
β’
β²π(π β§ π β β) |
171 | | nfv 1918 |
. . . . . . . 8
β’
β²π π£:(1...π)βΆπ |
172 | | nfv 1918 |
. . . . . . . 8
β’
β²π π· β βͺ ran π£ |
173 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π¦:(1...π)βΆπ |
174 | | nfra1 3266 |
. . . . . . . . . 10
β’
β²πβπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
175 | 173, 174 | nfan 1903 |
. . . . . . . . 9
β’
β²π(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
176 | 175 | nfex 2318 |
. . . . . . . 8
β’
β²πβπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
177 | 171, 172,
176 | nf3an 1905 |
. . . . . . 7
β’
β²π(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
178 | 170, 177 | nfan 1903 |
. . . . . 6
β’
β²π((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
179 | | nfv 1918 |
. . . . . . . 8
β’
β²π‘ π β β |
180 | 2, 179 | nfan 1903 |
. . . . . . 7
β’
β²π‘(π β§ π β β) |
181 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π‘π£ |
182 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π‘(1...π) |
183 | 181, 182,
131 | nff 6665 |
. . . . . . . 8
β’
β²π‘ π£:(1...π)βΆπ |
184 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π‘βͺ ran π£ |
185 | 3, 184 | nfss 3937 |
. . . . . . . 8
β’
β²π‘ π· β βͺ ran π£ |
186 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π‘π¦ |
187 | 123, 122 | nfrabw 3439 |
. . . . . . . . . . . 12
β’
β²π‘{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
188 | 150, 187 | nfcxfr 2902 |
. . . . . . . . . . 11
β’
β²π‘π |
189 | 186, 182,
188 | nff 6665 |
. . . . . . . . . 10
β’
β²π‘ π¦:(1...π)βΆπ |
190 | | nfra1 3266 |
. . . . . . . . . . . 12
β’
β²π‘βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) |
191 | | nfra1 3266 |
. . . . . . . . . . . 12
β’
β²π‘βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘) |
192 | 190, 191 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π‘(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
193 | 182, 192 | nfralw 3293 |
. . . . . . . . . 10
β’
β²π‘βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
194 | 189, 193 | nfan 1903 |
. . . . . . . . 9
β’
β²π‘(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
195 | 194 | nfex 2318 |
. . . . . . . 8
β’
β²π‘βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
196 | 183, 185,
195 | nf3an 1905 |
. . . . . . 7
β’
β²π‘(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
197 | 180, 196 | nfan 1903 |
. . . . . 6
β’
β²π‘((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
198 | | nfv 1918 |
. . . . . . 7
β’
β²π¦(π β§ π β β) |
199 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦ π£:(1...π)βΆπ |
200 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦ π· β βͺ ran π£ |
201 | | nfe1 2148 |
. . . . . . . 8
β’
β²π¦βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
202 | 199, 200,
201 | nf3an 1905 |
. . . . . . 7
β’
β²π¦(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
203 | 198, 202 | nfan 1903 |
. . . . . 6
β’
β²π¦((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
204 | | nfv 1918 |
. . . . . . 7
β’
β²π€(π β§ π β β) |
205 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π€π£ |
206 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π€(1...π) |
207 | 205, 206,
53 | nff 6665 |
. . . . . . . 8
β’
β²π€ π£:(1...π)βΆπ |
208 | | nfv 1918 |
. . . . . . . 8
β’
β²π€ π· β βͺ ran π£ |
209 | | nfv 1918 |
. . . . . . . 8
β’
β²π€βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
210 | 207, 208,
209 | nf3an 1905 |
. . . . . . 7
β’
β²π€(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
211 | 204, 210 | nfan 1903 |
. . . . . 6
β’
β²π€((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
212 | | eqid 2733 |
. . . . . 6
β’ {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
213 | | eqid 2733 |
. . . . . 6
β’ (π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}, π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) = (π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}, π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
214 | | eqid 2733 |
. . . . . 6
β’ (π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘))) = (π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘))) |
215 | | eqid 2733 |
. . . . . 6
β’ (π‘ β π β¦ (seq1( Β· , ((π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘)))βπ‘))βπ)) = (π‘ β π β¦ (seq1( Β· , ((π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘)))βπ‘))βπ)) |
216 | | simp1ll 1237 |
. . . . . . 7
β’ ((((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β§ π β π΄ β§ π β π΄) β π) |
217 | 216, 15 | syld3an1 1411 |
. . . . . 6
β’ ((((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
218 | 11 | sselda 3945 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π β πΆ) |
219 | 6, 9, 10, 218 | fcnre 43318 |
. . . . . . 7
β’ ((π β§ π β π΄) β π:πβΆβ) |
220 | 219 | ad4ant14 751 |
. . . . . 6
β’ ((((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β§ π β π΄) β π:πβΆβ) |
221 | | simplr 768 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π β β) |
222 | | simpr1 1195 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π£:(1...π)βΆπ) |
223 | 9 | cldss 22396 |
. . . . . . . 8
β’ (π΅ β (Clsdβπ½) β π΅ β π) |
224 | 22, 223 | syl 17 |
. . . . . . 7
β’ (π β π΅ β π) |
225 | 224 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π΅ β π) |
226 | | simpr2 1196 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π· β βͺ ran
π£) |
227 | 32 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π· β π) |
228 | | feq3 6652 |
. . . . . . . . . . . 12
β’ (π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β (π¦:(1...π)βΆπ β π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)})) |
229 | 150, 228 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π¦:(1...π)βΆπ β π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}) |
230 | 229 | biimpi 215 |
. . . . . . . . . 10
β’ (π¦:(1...π)βΆπ β π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}) |
231 | 230 | anim1i 616 |
. . . . . . . . 9
β’ ((π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) β (π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
232 | 231 | eximi 1838 |
. . . . . . . 8
β’
(βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) β βπ¦(π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
233 | 232 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ¦(π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
234 | 233 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β βπ¦(π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
235 | 7 | uniexd 7680 |
. . . . . . . 8
β’ (π β βͺ π½
β V) |
236 | 9, 235 | eqeltrid 2838 |
. . . . . . 7
β’ (π β π β V) |
237 | 236 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π β V) |
238 | 155 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β πΈ β
β+) |
239 | | stoweidlem57.21 |
. . . . . . 7
β’ (π β πΈ < (1 / 3)) |
240 | 239 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β πΈ < (1 / 3)) |
241 | 178, 197,
203, 211, 9, 212, 213, 214, 215, 44, 217, 220, 221, 222, 225, 226, 227, 234, 237, 238, 240 | stoweidlem54 44381 |
. . . . 5
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) |
242 | 241 | ex 414 |
. . . 4
β’ ((π β§ π β β) β ((π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
243 | 242 | exlimdv 1937 |
. . 3
β’ ((π β§ π β β) β (βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
244 | 243 | rexlimdva 3149 |
. 2
β’ (π β (βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
245 | 169, 244 | mpd 15 |
1
β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) |