Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . 5
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β π½ β
1stΟ) |
2 | | 1stctop 22810 |
. . . . . . 7
β’ (π½ β 1stΟ
β π½ β
Top) |
3 | | 1stcelcls.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
4 | 3 | clsss3 22426 |
. . . . . . 7
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β π) |
5 | 2, 4 | sylan 581 |
. . . . . 6
β’ ((π½ β 1stΟ
β§ π β π) β ((clsβπ½)βπ) β π) |
6 | 5 | sselda 3949 |
. . . . 5
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β π β π) |
7 | 3 | 1stcfb 22812 |
. . . . 5
β’ ((π½ β 1stΟ
β§ π β π) β βπ(π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) |
8 | 1, 6, 7 | syl2anc 585 |
. . . 4
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β βπ(π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) |
9 | | simpr2 1196 |
. . . . . . . . . . . 12
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ))) |
10 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β π β (πβπ)) |
11 | 10 | ralimi 3087 |
. . . . . . . . . . . 12
β’
(βπ β
β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β βπ β β π β (πβπ)) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . 11
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β βπ β β π β (πβπ)) |
13 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
14 | 13 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π = π β (π β (πβπ) β π β (πβπ))) |
15 | 14 | rspccva 3583 |
. . . . . . . . . . 11
β’
((βπ β
β π β (πβπ) β§ π β β) β π β (πβπ)) |
16 | 12, 15 | sylan 581 |
. . . . . . . . . 10
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β π β (πβπ)) |
17 | | eleq2 2827 |
. . . . . . . . . . . 12
β’ (π¦ = (πβπ) β (π β π¦ β π β (πβπ))) |
18 | | ineq1 4170 |
. . . . . . . . . . . . 13
β’ (π¦ = (πβπ) β (π¦ β© π) = ((πβπ) β© π)) |
19 | 18 | neeq1d 3004 |
. . . . . . . . . . . 12
β’ (π¦ = (πβπ) β ((π¦ β© π) β β
β ((πβπ) β© π) β β
)) |
20 | 17, 19 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π¦ = (πβπ) β ((π β π¦ β (π¦ β© π) β β
) β (π β (πβπ) β ((πβπ) β© π) β β
))) |
21 | 3 | elcls2 22441 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ π β π) β (π β ((clsβπ½)βπ) β (π β π β§ βπ¦ β π½ (π β π¦ β (π¦ β© π) β β
)))) |
22 | 2, 21 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π½ β 1stΟ
β§ π β π) β (π β ((clsβπ½)βπ) β (π β π β§ βπ¦ β π½ (π β π¦ β (π¦ β© π) β β
)))) |
23 | 22 | simplbda 501 |
. . . . . . . . . . . 12
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β βπ¦ β π½ (π β π¦ β (π¦ β© π) β β
)) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β βπ¦ β π½ (π β π¦ β (π¦ β© π) β β
)) |
25 | | simpr1 1195 |
. . . . . . . . . . . 12
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β π:ββΆπ½) |
26 | 25 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β (πβπ) β π½) |
27 | 20, 24, 26 | rspcdva 3585 |
. . . . . . . . . 10
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β (π β (πβπ) β ((πβπ) β© π) β β
)) |
28 | 16, 27 | mpd 15 |
. . . . . . . . 9
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β ((πβπ) β© π) β β
) |
29 | | elin 3931 |
. . . . . . . . . . . 12
β’ (π₯ β ((πβπ) β© π) β (π₯ β (πβπ) β§ π₯ β π)) |
30 | 29 | biancomi 464 |
. . . . . . . . . . 11
β’ (π₯ β ((πβπ) β© π) β (π₯ β π β§ π₯ β (πβπ))) |
31 | 30 | exbii 1851 |
. . . . . . . . . 10
β’
(βπ₯ π₯ β ((πβπ) β© π) β βπ₯(π₯ β π β§ π₯ β (πβπ))) |
32 | | n0 4311 |
. . . . . . . . . 10
β’ (((πβπ) β© π) β β
β βπ₯ π₯ β ((πβπ) β© π)) |
33 | | df-rex 3075 |
. . . . . . . . . 10
β’
(βπ₯ β
π π₯ β (πβπ) β βπ₯(π₯ β π β§ π₯ β (πβπ))) |
34 | 31, 32, 33 | 3bitr4i 303 |
. . . . . . . . 9
β’ (((πβπ) β© π) β β
β βπ₯ β π π₯ β (πβπ)) |
35 | 28, 34 | sylib 217 |
. . . . . . . 8
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β βπ₯ β π π₯ β (πβπ)) |
36 | 2 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β π½ β Top) |
37 | 3 | topopn 22271 |
. . . . . . . . . . . . 13
β’ (π½ β Top β π β π½) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β π β π½) |
39 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β π β π) |
40 | 38, 39 | ssexd 5286 |
. . . . . . . . . . 11
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β π β V) |
41 | | fvi 6922 |
. . . . . . . . . . 11
β’ (π β V β ( I
βπ) = π) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β ( I βπ) = π) |
43 | 42 | ad2antrr 725 |
. . . . . . . . 9
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β ( I βπ) = π) |
44 | 43 | rexeqdv 3317 |
. . . . . . . 8
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β (βπ₯ β ( I βπ)π₯ β (πβπ) β βπ₯ β π π₯ β (πβπ))) |
45 | 35, 44 | mpbird 257 |
. . . . . . 7
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π β β) β βπ₯ β ( I βπ)π₯ β (πβπ)) |
46 | 45 | ralrimiva 3144 |
. . . . . 6
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β βπ β β βπ₯ β ( I βπ)π₯ β (πβπ)) |
47 | | fvex 6860 |
. . . . . . 7
β’ ( I
βπ) β
V |
48 | | nnenom 13892 |
. . . . . . 7
β’ β
β Ο |
49 | | eleq1 2826 |
. . . . . . 7
β’ (π₯ = (πβπ) β (π₯ β (πβπ) β (πβπ) β (πβπ))) |
50 | 47, 48, 49 | axcc4 10382 |
. . . . . 6
β’
(βπ β
β βπ₯ β ( I
βπ)π₯ β (πβπ) β βπ(π:ββΆ( I βπ) β§ βπ β β (πβπ) β (πβπ))) |
51 | 46, 50 | syl 17 |
. . . . 5
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β βπ(π:ββΆ( I βπ) β§ βπ β β (πβπ) β (πβπ))) |
52 | 42 | feq3d 6660 |
. . . . . . . . 9
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β (π:ββΆ( I βπ) β π:ββΆπ)) |
53 | 52 | biimpd 228 |
. . . . . . . 8
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β (π:ββΆ( I βπ) β π:ββΆπ)) |
54 | 53 | adantr 482 |
. . . . . . 7
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β (π:ββΆ( I βπ) β π:ββΆπ)) |
55 | 6 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β π β π) |
56 | | simplr3 1218 |
. . . . . . . . . . . . 13
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯)) |
57 | | eleq2 2827 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (π β π₯ β π β π¦)) |
58 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πβπ) = (πβπ)) |
59 | 58 | sseq1d 3980 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πβπ) β π₯ β (πβπ) β π₯)) |
60 | 59 | cbvrexvw 3229 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
β (πβπ) β π₯ β βπ β β (πβπ) β π₯) |
61 | | sseq2 3975 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β ((πβπ) β π₯ β (πβπ) β π¦)) |
62 | 61 | rexbidv 3176 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (βπ β β (πβπ) β π₯ β βπ β β (πβπ) β π¦)) |
63 | 60, 62 | bitrid 283 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (βπ β β (πβπ) β π₯ β βπ β β (πβπ) β π¦)) |
64 | 57, 63 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β ((π β π₯ β βπ β β (πβπ) β π₯) β (π β π¦ β βπ β β (πβπ) β π¦))) |
65 | 64 | rspccva 3583 |
. . . . . . . . . . . . 13
β’
((βπ₯ β
π½ (π β π₯ β βπ β β (πβπ) β π₯) β§ π¦ β π½) β (π β π¦ β βπ β β (πβπ) β π¦)) |
66 | 56, 65 | sylan 581 |
. . . . . . . . . . . 12
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β§ π¦ β π½) β (π β π¦ β βπ β β (πβπ) β π¦)) |
67 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β (πβ(π + 1)) β (πβπ)) |
68 | 67 | ralimi 3087 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β βπ β β (πβ(π + 1)) β (πβπ)) |
69 | 9, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β βπ β β (πβ(π + 1)) β (πβπ)) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β βπ β β (πβ(π + 1)) β (πβπ)) |
71 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β π β β) |
72 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (πβπ) = (πβπ)) |
73 | 72 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β ((πβπ) β (πβπ) β (πβπ) β (πβπ))) |
74 | 73 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ)) β ((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ)))) |
75 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (πβπ) = (πβπ)) |
76 | 75 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β ((πβπ) β (πβπ) β (πβπ) β (πβπ))) |
77 | 76 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ)) β ((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ)))) |
78 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
79 | 78 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π + 1) β ((πβπ) β (πβπ) β (πβ(π + 1)) β (πβπ))) |
80 | 79 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π + 1) β (((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ)) β ((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβ(π + 1)) β (πβπ)))) |
81 | | ssid 3971 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πβπ) β (πβπ) |
82 | 81 | 2a1i 12 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β€ β
((βπ β β
(πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ))) |
83 | | eluznn 12850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
84 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
85 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β (πβπ) = (πβπ)) |
86 | 84, 85 | sseq12d 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β ((πβ(π + 1)) β (πβπ) β (πβ(π + 1)) β (πβπ))) |
87 | 86 | rspccva 3583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((βπ β
β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβ(π + 1)) β (πβπ)) |
88 | 83, 87 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((βπ β
β (πβ(π + 1)) β (πβπ) β§ (π β β β§ π β (β€β₯βπ))) β (πβ(π + 1)) β (πβπ)) |
89 | 88 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((βπ β
β (πβ(π + 1)) β (πβπ) β§ π β β) β§ π β (β€β₯βπ)) β (πβ(π + 1)) β (πβπ)) |
90 | | sstr2 3956 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πβ(π + 1)) β (πβπ) β ((πβπ) β (πβπ) β (πβ(π + 1)) β (πβπ))) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((βπ β
β (πβ(π + 1)) β (πβπ) β§ π β β) β§ π β (β€β₯βπ)) β ((πβπ) β (πβπ) β (πβ(π + 1)) β (πβπ))) |
92 | 91 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯βπ) β ((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β ((πβπ) β (πβπ) β (πβ(π + 1)) β (πβπ)))) |
93 | 92 | a2d 29 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(β€β₯βπ) β (((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ)) β ((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβ(π + 1)) β (πβπ)))) |
94 | 74, 77, 80, 77, 82, 93 | uzind4 12838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯βπ) β ((βπ β β (πβ(π + 1)) β (πβπ) β§ π β β) β (πβπ) β (πβπ))) |
95 | 94 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
β (πβ(π + 1)) β (πβπ) β§ π β β) β (π β (β€β₯βπ) β (πβπ) β (πβπ))) |
96 | 95 | ralrimiv 3143 |
. . . . . . . . . . . . . . . . . . 19
β’
((βπ β
β (πβ(π + 1)) β (πβπ) β§ π β β) β βπ β
(β€β₯βπ)(πβπ) β (πβπ)) |
97 | 70, 71, 96 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β βπ β
(β€β₯βπ)(πβπ) β (πβπ)) |
98 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πβπ) = (πβπ)) |
99 | 98, 75 | eleq12d 2832 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πβπ) β (πβπ) β (πβπ) β (πβπ))) |
100 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β)) β βπ β β (πβπ) β (πβπ)) |
101 | 100 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β§ π β (β€β₯βπ)) β βπ β β (πβπ) β (πβπ)) |
102 | 71, 83 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β§ π β (β€β₯βπ)) β π β β) |
103 | 99, 101, 102 | rspcdva 3585 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β§ π β (β€β₯βπ)) β (πβπ) β (πβπ)) |
104 | 103 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β βπ β
(β€β₯βπ)(πβπ) β (πβπ)) |
105 | | r19.26 3115 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(β€β₯βπ)((πβπ) β (πβπ) β§ (πβπ) β (πβπ)) β (βπ β (β€β₯βπ)(πβπ) β (πβπ) β§ βπ β (β€β₯βπ)(πβπ) β (πβπ))) |
106 | 97, 104, 105 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β βπ β
(β€β₯βπ)((πβπ) β (πβπ) β§ (πβπ) β (πβπ))) |
107 | | ssel2 3944 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ) β (πβπ) β§ (πβπ) β (πβπ)) β (πβπ) β (πβπ)) |
108 | 107 | ralimi 3087 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(β€β₯βπ)((πβπ) β (πβπ) β§ (πβπ) β (πβπ)) β βπ β (β€β₯βπ)(πβπ) β (πβπ)) |
109 | 106, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β βπ β
(β€β₯βπ)(πβπ) β (πβπ)) |
110 | | ssel 3942 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ) β π¦ β ((πβπ) β (πβπ) β (πβπ) β π¦)) |
111 | 110 | ralimdv 3167 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β π¦ β (βπ β (β€β₯βπ)(πβπ) β (πβπ) β βπ β (β€β₯βπ)(πβπ) β π¦)) |
112 | 109, 111 | syl5com 31 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β§ (π¦ β π½ β§ π β β))) β ((πβπ) β π¦ β βπ β (β€β₯βπ)(πβπ) β π¦)) |
113 | 112 | anassrs 469 |
. . . . . . . . . . . . . 14
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β§ (π¦ β π½ β§ π β β)) β ((πβπ) β π¦ β βπ β (β€β₯βπ)(πβπ) β π¦)) |
114 | 113 | anassrs 469 |
. . . . . . . . . . . . 13
β’
(((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β§ π¦ β π½) β§ π β β) β ((πβπ) β π¦ β βπ β (β€β₯βπ)(πβπ) β π¦)) |
115 | 114 | reximdva 3166 |
. . . . . . . . . . . 12
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β§ π¦ β π½) β (βπ β β (πβπ) β π¦ β βπ β β βπ β (β€β₯βπ)(πβπ) β π¦)) |
116 | 66, 115 | syld 47 |
. . . . . . . . . . 11
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β§ π¦ β π½) β (π β π¦ β βπ β β βπ β (β€β₯βπ)(πβπ) β π¦)) |
117 | 116 | ralrimiva 3144 |
. . . . . . . . . 10
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β βπ¦ β π½ (π β π¦ β βπ β β βπ β (β€β₯βπ)(πβπ) β π¦)) |
118 | 36 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β π½ β Top) |
119 | 3 | toptopon 22282 |
. . . . . . . . . . . 12
β’ (π½ β Top β π½ β (TopOnβπ)) |
120 | 118, 119 | sylib 217 |
. . . . . . . . . . 11
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β π½ β (TopOnβπ)) |
121 | | nnuz 12813 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
122 | | 1zzd 12541 |
. . . . . . . . . . 11
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β 1 β β€) |
123 | | simprl 770 |
. . . . . . . . . . . 12
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β π:ββΆπ) |
124 | 39 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β π β π) |
125 | 123, 124 | fssd 6691 |
. . . . . . . . . . 11
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β π:ββΆπ) |
126 | | eqidd 2738 |
. . . . . . . . . . 11
β’
((((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β§ π β β) β (πβπ) = (πβπ)) |
127 | 120, 121,
122, 125, 126 | lmbrf 22627 |
. . . . . . . . . 10
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β (π(βπ‘βπ½)π β (π β π β§ βπ¦ β π½ (π β π¦ β βπ β β βπ β (β€β₯βπ)(πβπ) β π¦)))) |
128 | 55, 117, 127 | mpbir2and 712 |
. . . . . . . . 9
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ (π:ββΆπ β§ βπ β β (πβπ) β (πβπ))) β π(βπ‘βπ½)π) |
129 | 128 | expr 458 |
. . . . . . . 8
β’
(((((π½ β
1stΟ β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β§ π:ββΆπ) β (βπ β β (πβπ) β (πβπ) β π(βπ‘βπ½)π)) |
130 | 129 | imdistanda 573 |
. . . . . . 7
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β ((π:ββΆπ β§ βπ β β (πβπ) β (πβπ)) β (π:ββΆπ β§ π(βπ‘βπ½)π))) |
131 | 54, 130 | syland 604 |
. . . . . 6
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β ((π:ββΆ( I βπ) β§ βπ β β (πβπ) β (πβπ)) β (π:ββΆπ β§ π(βπ‘βπ½)π))) |
132 | 131 | eximdv 1921 |
. . . . 5
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β (βπ(π:ββΆ( I βπ) β§ βπ β β (πβπ) β (πβπ)) β βπ(π:ββΆπ β§ π(βπ‘βπ½)π))) |
133 | 51, 132 | mpd 15 |
. . . 4
β’ ((((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β§ (π:ββΆπ½ β§ βπ β β (π β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ₯ β π½ (π β π₯ β βπ β β (πβπ) β π₯))) β βπ(π:ββΆπ β§ π(βπ‘βπ½)π)) |
134 | 8, 133 | exlimddv 1939 |
. . 3
β’ (((π½ β 1stΟ
β§ π β π) β§ π β ((clsβπ½)βπ)) β βπ(π:ββΆπ β§ π(βπ‘βπ½)π)) |
135 | 134 | ex 414 |
. 2
β’ ((π½ β 1stΟ
β§ π β π) β (π β ((clsβπ½)βπ) β βπ(π:ββΆπ β§ π(βπ‘βπ½)π))) |
136 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β π½ β Top) |
137 | 136, 119 | sylib 217 |
. . . . 5
β’ (((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β π½ β (TopOnβπ)) |
138 | | 1zzd 12541 |
. . . . 5
β’ (((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β 1 β β€) |
139 | | simprr 772 |
. . . . 5
β’ (((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β π(βπ‘βπ½)π) |
140 | | simprl 770 |
. . . . . 6
β’ (((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β π:ββΆπ) |
141 | 140 | ffvelcdmda 7040 |
. . . . 5
β’ ((((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β§ π β β) β (πβπ) β π) |
142 | | simplr 768 |
. . . . 5
β’ (((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β π β π) |
143 | 121, 137,
138, 139, 141, 142 | lmcls 22669 |
. . . 4
β’ (((π½ β 1stΟ
β§ π β π) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β π β ((clsβπ½)βπ)) |
144 | 143 | ex 414 |
. . 3
β’ ((π½ β 1stΟ
β§ π β π) β ((π:ββΆπ β§ π(βπ‘βπ½)π) β π β ((clsβπ½)βπ))) |
145 | 144 | exlimdv 1937 |
. 2
β’ ((π½ β 1stΟ
β§ π β π) β (βπ(π:ββΆπ β§ π(βπ‘βπ½)π) β π β ((clsβπ½)βπ))) |
146 | 135, 145 | impbid 211 |
1
β’ ((π½ β 1stΟ
β§ π β π) β (π β ((clsβπ½)βπ) β βπ(π:ββΆπ β§ π(βπ‘βπ½)π))) |