Step | Hyp | Ref
| Expression |
1 | | pibt2.x |
. . . 4
β’ π = βͺ
π½ |
2 | | pibt2.19 |
. . . 4
β’ πΆ = {π₯ β Top β£ βπ¦ β π« π₯((βͺ
π₯ = βͺ π¦
β§ π¦ βΌ Ο)
β βπ§ β
(π« π¦ β©
Fin)βͺ π₯ = βͺ π§)} |
3 | 1, 2 | pibp19 35914 |
. . 3
β’ (π½ β πΆ β (π½ β Top β§ βπ¦ β π« π½((π = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |
4 | 3 | simplbi 499 |
. 2
β’ (π½ β πΆ β π½ β Top) |
5 | | eldif 3925 |
. . . . 5
β’ (π β (π« π β Fin) β (π β π« π β§ Β¬ π β Fin)) |
6 | | velpw 4570 |
. . . . . . 7
β’ (π β π« π β π β π) |
7 | 6 | anbi1i 625 |
. . . . . 6
β’ ((π β π« π β§ Β¬ π β Fin) β (π β π β§ Β¬ π β Fin)) |
8 | | vex 3452 |
. . . . . . . . . 10
β’ π β V |
9 | | infinf 10509 |
. . . . . . . . . 10
β’ (π β V β (Β¬ π β Fin β Ο
βΌ π)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . 9
β’ (Β¬
π β Fin β Ο
βΌ π) |
11 | 8 | infcntss 9272 |
. . . . . . . . 9
β’ (Ο
βΌ π β
βπ(π β π β§ π β Ο)) |
12 | 10, 11 | sylbi 216 |
. . . . . . . 8
β’ (Β¬
π β Fin β
βπ(π β π β§ π β Ο)) |
13 | 12 | ad2antll 728 |
. . . . . . 7
β’ ((π½ β πΆ β§ (π β π β§ Β¬ π β Fin)) β βπ(π β π β§ π β Ο)) |
14 | | sstr 3957 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β π β π) |
15 | 14 | ancoms 460 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β π β π) |
16 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ ((limPtβπ½)βπ) = β
)) β π β Ο) |
17 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ β πΆ β§ π β Ο) β§ π β π) β§ ((limPtβπ½)βπ) = β
) β (π½ β πΆ β§ π β Ο)) |
18 | | 0ss 4361 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ β
β π |
19 | | sseq1 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((limPtβπ½)βπ) = β
β (((limPtβπ½)βπ) β π β β
β π)) |
20 | 18, 19 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((limPtβπ½)βπ) = β
β ((limPtβπ½)βπ) β π) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π½ β Top β§ π β π) β§ ((limPtβπ½)βπ) = β
) β ((limPtβπ½)βπ) β π) |
22 | 1 | cldlp 22517 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π½ β Top β§ π β π) β (π β (Clsdβπ½) β ((limPtβπ½)βπ) β π)) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π½ β Top β§ π β π) β§ ((limPtβπ½)βπ) = β
) β (π β (Clsdβπ½) β ((limPtβπ½)βπ) β π)) |
24 | 21, 23 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π½ β Top β§ π β π) β§ ((limPtβπ½)βπ) = β
) β π β (Clsdβπ½)) |
25 | 4, 24 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π½ β πΆ β§ π β π) β§ ((limPtβπ½)βπ) = β
) β π β (Clsdβπ½)) |
26 | 25 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ β πΆ β§ π β Ο) β§ π β π) β§ ((limPtβπ½)βπ) = β
) β π β (Clsdβπ½)) |
27 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ β πΆ β§ π β Ο) β§ π β π) β§ ((limPtβπ½)βπ) = β
) β ((limPtβπ½)βπ) = β
) |
28 | 1 | cldss 22396 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (Clsdβπ½) β π β π) |
29 | 1 | nlpineqsn 35908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π½ β Top β§ π β π β§ ((limPtβπ½)βπ) = β
) β βπ β π βπ β π½ (π β π β§ (π β© π) = {π})) |
30 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β π β§ (π β© π) = {π}) β (π β© π) = {π}) |
31 | 30 | reximi 3088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ β
π½ (π β π β§ (π β© π) = {π}) β βπ β π½ (π β© π) = {π}) |
32 | 31 | ralimi 3087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ β
π βπ β π½ (π β π β§ (π β© π) = {π}) β βπ β π βπ β π½ (π β© π) = {π}) |
33 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π β V |
34 | | ineq1 4170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = (πβπ) β (π β© π) = ((πβπ) β© π)) |
35 | 34 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (πβπ) β ((π β© π) = {π} β ((πβπ) β© π) = {π})) |
36 | 33, 35 | ac6s 10427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ β
π βπ β π½ (π β© π) = {π} β βπ(π:πβΆπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
37 | 29, 32, 36 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π½ β Top β§ π β π β§ ((limPtβπ½)βπ) = β
) β βπ(π:πβΆπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
38 | | fvineqsnf1 35910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π:πβΆπ½ β§ βπ β π ((πβπ) β© π) = {π}) β π:πβ1-1βπ½) |
39 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π:πβΆπ½ β§ βπ β π ((πβπ) β© π) = {π}) β βπ β π ((πβπ) β© π) = {π}) |
40 | 38, 39 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π:πβΆπ½ β§ βπ β π ((πβπ) β© π) = {π}) β (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
41 | 40 | eximi 1838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ(π:πβΆπ½ β§ βπ β π ((πβπ) β© π) = {π}) β βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
42 | 37, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π½ β Top β§ π β π β§ ((limPtβπ½)βπ) = β
) β βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
43 | 28, 42 | syl3an2 1165 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π½ β Top β§ π β (Clsdβπ½) β§ ((limPtβπ½)βπ) = β
) β βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
44 | 4, 43 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π½ β πΆ β§ π β (Clsdβπ½) β§ ((limPtβπ½)βπ) = β
) β βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
45 | 44 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π½ β πΆ β§ π β Ο) β§ π β (Clsdβπ½) β§ ((limPtβπ½)βπ) = β
) β βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) |
46 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π½ β Top β§ π β (Clsdβπ½)) β§ π:πβ1-1βπ½) β π:πβ1-1βπ½) |
47 | | vsnid 4628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ π β {π} |
48 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((πβπ) β© π) = {π} β (π β ((πβπ) β© π) β π β {π})) |
49 | 47, 48 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((πβπ) β© π) = {π} β π β ((πβπ) β© π)) |
50 | 49 | elin1d 4163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((πβπ) β© π) = {π} β π β (πβπ)) |
51 | 50 | ralimi 3087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(βπ β
π ((πβπ) β© π) = {π} β βπ β π π β (πβπ)) |
52 | | ralssiun 35907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(βπ β
π π β (πβπ) β π β βͺ
π β π (πβπ)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(βπ β
π ((πβπ) β© π) = {π} β π β βͺ
π β π (πβπ)) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β π β βͺ
π β π (πβπ)) |
55 | | f1fn 6744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π:πβ1-1βπ½ β π Fn π) |
56 | | fniunfv 7199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π Fn π β βͺ
π β π (πβπ) = βͺ ran π) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π:πβ1-1βπ½ β βͺ
π β π (πβπ) = βͺ ran π) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β βͺ
π β π (πβπ) = βͺ ran π) |
59 | 54, 58 | sseqtrd 3989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β π β βͺ ran
π) |
60 | 1 | cldopn 22398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β (Clsdβπ½) β (π β π) β π½) |
61 | 60 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β (π β π) β π½) |
62 | 61 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ π β βͺ ran
π) β ((π β π) β π½ β§ π β βͺ ran
π)) |
63 | 62 | ancomd 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ π β βͺ ran
π) β (π β βͺ ran π β§ (π β π) β π½)) |
64 | 28 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β π β π) |
65 | 64 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ (π β βͺ ran
π β§ (π β π) β π½)) β (π β π β§ (π β βͺ ran
π β§ (π β π) β π½))) |
66 | | unisng 4891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β π) β π½ β βͺ {(π β π)} = (π β π)) |
67 | 66 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β π) β π½ β (π β π) = βͺ {(π β π)}) |
68 | | eqimss 4005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β π) = βͺ {(π β π)} β (π β π) β βͺ
{(π β π)}) |
69 | | ssun4 4140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β π) β βͺ
{(π β π)} β (π β π) β (βͺ ran
π βͺ βͺ {(π
β π)})) |
70 | | uniun 4896 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ βͺ (ran π βͺ {(π β π)}) = (βͺ ran π βͺ βͺ {(π
β π)}) |
71 | 69, 70 | sseqtrrdi 4000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β π) β βͺ
{(π β π)} β (π β π) β βͺ (ran
π βͺ {(π β π)})) |
72 | 67, 68, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β π) β π½ β (π β π) β βͺ (ran
π βͺ {(π β π)})) |
73 | | ssun3 4139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π β βͺ ran π β π β (βͺ ran
π βͺ βͺ {(π
β π)})) |
74 | 73, 70 | sseqtrrdi 4000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π β βͺ ran π β π β βͺ (ran
π βͺ {(π β π)})) |
75 | | uncom 4118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π βͺ (π β π)) = ((π β π) βͺ π) |
76 | | undif1 4440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π β π) βͺ π) = (π βͺ π) |
77 | 75, 76 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π βͺ (π β π)) = (π βͺ π) |
78 | | ssequn2 4148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π β π β (π βͺ π) = π) |
79 | 78 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π β π β (π βͺ π) = π) |
80 | 77, 79 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π β π β (π βͺ (π β π)) = π) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β π β§ (π β βͺ (ran
π βͺ {(π β π)}) β§ (π β π) β βͺ (ran
π βͺ {(π β π)}))) β (π βͺ (π β π)) = π) |
82 | | unss12 4147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β βͺ (ran π βͺ {(π β π)}) β§ (π β π) β βͺ (ran
π βͺ {(π β π)})) β (π βͺ (π β π)) β (βͺ (ran
π βͺ {(π β π)}) βͺ βͺ (ran
π βͺ {(π β π)}))) |
83 | | unidm 4117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (βͺ (ran π βͺ {(π β π)}) βͺ βͺ (ran
π βͺ {(π β π)})) = βͺ (ran
π βͺ {(π β π)}) |
84 | 82, 83 | sseqtrdi 3999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β βͺ (ran π βͺ {(π β π)}) β§ (π β π) β βͺ (ran
π βͺ {(π β π)})) β (π βͺ (π β π)) β βͺ (ran
π βͺ {(π β π)})) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β π β§ (π β βͺ (ran
π βͺ {(π β π)}) β§ (π β π) β βͺ (ran
π βͺ {(π β π)}))) β (π βͺ (π β π)) β βͺ (ran
π βͺ {(π β π)})) |
86 | 81, 85 | eqsstrrd 3988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β π β§ (π β βͺ (ran
π βͺ {(π β π)}) β§ (π β π) β βͺ (ran
π βͺ {(π β π)}))) β π β βͺ (ran
π βͺ {(π β π)})) |
87 | 74, 86 | sylanr1 681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β π β§ (π β βͺ ran
π β§ (π β π) β βͺ (ran
π βͺ {(π β π)}))) β π β βͺ (ran
π βͺ {(π β π)})) |
88 | 72, 87 | sylanr2 682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β π β§ (π β βͺ ran
π β§ (π β π) β π½)) β π β βͺ (ran
π βͺ {(π β π)})) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ (π β π β§ (π β βͺ ran
π β§ (π β π) β π½))) β π β βͺ (ran
π βͺ {(π β π)})) |
90 | | f1f 6743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π:πβ1-1βπ½ β π:πβΆπ½) |
91 | | frn 6680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π:πβΆπ½ β ran π β π½) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π:πβ1-1βπ½ β ran π β π½) |
93 | 1 | topopn 22271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π½ β Top β π β π½) |
94 | 1 | difopn 22401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β π½ β§ π β (Clsdβπ½)) β (π β π) β π½) |
95 | 93, 94 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π½ β Top β§ π β (Clsdβπ½)) β (π β π) β π½) |
96 | 95 | snssd 4774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π½ β Top β§ π β (Clsdβπ½)) β {(π β π)} β π½) |
97 | | unss12 4147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((ran
π β π½ β§ {(π β π)} β π½) β (ran π βͺ {(π β π)}) β (π½ βͺ π½)) |
98 | | unidm 4117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π½ βͺ π½) = π½ |
99 | 97, 98 | sseqtrdi 3999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((ran
π β π½ β§ {(π β π)} β π½) β (ran π βͺ {(π β π)}) β π½) |
100 | 92, 96, 99 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β (ran π βͺ {(π β π)}) β π½) |
101 | | uniss 4878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((ran
π βͺ {(π β π)}) β π½ β βͺ (ran
π βͺ {(π β π)}) β βͺ
π½) |
102 | 101, 1 | sseqtrrdi 4000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((ran
π βͺ {(π β π)}) β π½ β βͺ (ran
π βͺ {(π β π)}) β π) |
103 | 100, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β βͺ (ran
π βͺ {(π β π)}) β π) |
104 | 103 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ (π β π β§ (π β βͺ ran
π β§ (π β π) β π½))) β βͺ (ran
π βͺ {(π β π)}) β π) |
105 | 89, 104 | eqssd 3966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ (π β π β§ (π β βͺ ran
π β§ (π β π) β π½))) β π = βͺ (ran π βͺ {(π β π)})) |
106 | 65, 105 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ (π β βͺ ran
π β§ (π β π) β π½)) β π = βͺ (ran π βͺ {(π β π)})) |
107 | 63, 106 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ π β βͺ ran
π) β π = βͺ (ran π βͺ {(π β π)})) |
108 | 59, 107 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π:πβ1-1βπ½ β§ (π½ β Top β§ π β (Clsdβπ½))) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β π = βͺ (ran π βͺ {(π β π)})) |
109 | 108 | ancom1s 652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π½ β Top β§ π β (Clsdβπ½)) β§ π:πβ1-1βπ½) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β π = βͺ (ran π βͺ {(π β π)})) |
110 | 109 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π½ β Top β§ π β (Clsdβπ½)) β§ π:πβ1-1βπ½) β ((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β π = βͺ (ran π βͺ {(π β π)}))) |
111 | 46, 110 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π½ β Top β§ π β (Clsdβπ½)) β§ π:πβ1-1βπ½) β (βπ β π ((πβπ) β© π) = {π} β π = βͺ (ran π βͺ {(π β π)}))) |
112 | 111 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π½ β Top β§ π β (Clsdβπ½)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β π = βͺ (ran π βͺ {(π β π)})) |
113 | 112 | adantlrr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π½ β Top β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β π = βͺ (ran π βͺ {(π β π)})) |
114 | 4, 113 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β π = βͺ (ran π βͺ {(π β π)})) |
115 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ π β V |
116 | | f1f1orn 6800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π:πβ1-1βπ½ β π:πβ1-1-ontoβran
π) |
117 | | f1oen3g 8913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β V β§ π:πβ1-1-ontoβran
π) β π β ran π) |
118 | 115, 116,
117 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π:πβ1-1βπ½ β π β ran π) |
119 | | enen1 9068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β ran π β (π β Ο β ran π β
Ο)) |
120 | | endom 8926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (ran
π β Ο β
ran π βΌ
Ο) |
121 | | snfi 8995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ {(π β π)} β Fin |
122 | | isfinite 9595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ({(π β π)} β Fin β {(π β π)} βΊ Ο) |
123 | 121, 122 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ {(π β π)} βΊ Ο |
124 | | sdomdom 8927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ({(π β π)} βΊ Ο β {(π β π)} βΌ Ο) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ {(π β π)} βΌ Ο |
126 | | unctb 10148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((ran
π βΌ Ο β§
{(π β π)} βΌ Ο) β (ran
π βͺ {(π β π)}) βΌ Ο) |
127 | 120, 125,
126 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (ran
π β Ο β
(ran π βͺ {(π β π)}) βΌ Ο) |
128 | 119, 127 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β ran π β (π β Ο β (ran π βͺ {(π β π)}) βΌ Ο)) |
129 | 118, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π:πβ1-1βπ½ β (π β Ο β (ran π βͺ {(π β π)}) βΌ Ο)) |
130 | 129 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β Ο β§ π:πβ1-1βπ½) β (ran π βͺ {(π β π)}) βΌ Ο) |
131 | 130 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β (Clsdβπ½) β§ π β Ο) β§ π:πβ1-1βπ½) β (ran π βͺ {(π β π)}) βΌ Ο) |
132 | 131 | ad2ant2lr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β (ran π βͺ {(π β π)}) βΌ Ο) |
133 | 100 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π½ β Top β§ π β (Clsdβπ½)) β§ π:πβ1-1βπ½) β (ran π βͺ {(π β π)}) β π½) |
134 | 133 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π½ β Top β§ π β (Clsdβπ½)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β (ran π βͺ {(π β π)}) β π½) |
135 | 134 | adantlrr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π½ β Top β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β (ran π βͺ {(π β π)}) β π½) |
136 | 4, 135 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β (ran π βͺ {(π β π)}) β π½) |
137 | | elpw2g 5306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π½ β πΆ β ((ran π βͺ {(π β π)}) β π« π½ β (ran π βͺ {(π β π)}) β π½)) |
138 | 137 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π½ β πΆ β ((ran π βͺ {(π β π)}) β π½ β (ran π βͺ {(π β π)}) β π« π½)) |
139 | 138 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β ((ran π βͺ {(π β π)}) β π½ β (ran π βͺ {(π β π)}) β π« π½)) |
140 | 136, 139 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β (ran π βͺ {(π β π)}) β π« π½) |
141 | 3 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π½ β πΆ β βπ¦ β π« π½((π = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)π = βͺ π§)) |
142 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = π§ β βͺ π = βͺ
π§) |
143 | 142 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π§ β (π = βͺ π β π = βͺ π§)) |
144 | 143 | cbvrexvw 3229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(βπ β
(π« π¦ β©
Fin)π = βͺ π
β βπ§ β
(π« π¦ β©
Fin)π = βͺ π§) |
145 | 144 | imbi2i 336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π = βͺ
π¦ β§ π¦ βΌ Ο) β βπ β (π« π¦ β© Fin)π = βͺ π ) β ((π = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)π = βͺ π§)) |
146 | 145 | ralbii 3097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(βπ¦ β
π« π½((π = βͺ
π¦ β§ π¦ βΌ Ο) β βπ β (π« π¦ β© Fin)π = βͺ π ) β βπ¦ β π« π½((π = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)π = βͺ π§)) |
147 | 141, 146 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π½ β πΆ β βπ¦ β π« π½((π = βͺ π¦ β§ π¦ βΌ Ο) β βπ β (π« π¦ β© Fin)π = βͺ π )) |
148 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π¦ = (ran π βͺ {(π β π)}) β βͺ π¦ = βͺ
(ran π βͺ {(π β π)})) |
149 | 148 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ = (ran π βͺ {(π β π)}) β (π = βͺ π¦ β π = βͺ (ran π βͺ {(π β π)}))) |
150 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ = (ran π βͺ {(π β π)}) β (π¦ βΌ Ο β (ran π βͺ {(π β π)}) βΌ Ο)) |
151 | 149, 150 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π¦ = (ran π βͺ {(π β π)}) β ((π = βͺ π¦ β§ π¦ βΌ Ο) β (π = βͺ (ran π βͺ {(π β π)}) β§ (ran π βͺ {(π β π)}) βΌ Ο))) |
152 | | pweq 4579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π¦ = (ran π βͺ {(π β π)}) β π« π¦ = π« (ran π βͺ {(π β π)})) |
153 | 152 | ineq1d 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ = (ran π βͺ {(π β π)}) β (π« π¦ β© Fin) = (π« (ran π βͺ {(π β π)}) β© Fin)) |
154 | 153 | rexeqdv 3317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π¦ = (ran π βͺ {(π β π)}) β (βπ β (π« π¦ β© Fin)π = βͺ π β βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π )) |
155 | 151, 154 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π¦ = (ran π βͺ {(π β π)}) β (((π = βͺ π¦ β§ π¦ βΌ Ο) β βπ β (π« π¦ β© Fin)π = βͺ π ) β ((π = βͺ (ran π βͺ {(π β π)}) β§ (ran π βͺ {(π β π)}) βΌ Ο) β βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π ))) |
156 | 155 | rspccv 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(βπ¦ β
π« π½((π = βͺ
π¦ β§ π¦ βΌ Ο) β βπ β (π« π¦ β© Fin)π = βͺ π ) β ((ran π βͺ {(π β π)}) β π« π½ β ((π = βͺ (ran π βͺ {(π β π)}) β§ (ran π βͺ {(π β π)}) βΌ Ο) β βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π ))) |
157 | 147, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π½ β πΆ β ((ran π βͺ {(π β π)}) β π« π½ β ((π = βͺ (ran π βͺ {(π β π)}) β§ (ran π βͺ {(π β π)}) βΌ Ο) β βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π ))) |
158 | 157 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β ((ran π βͺ {(π β π)}) β π« π½ β ((π = βͺ (ran π βͺ {(π β π)}) β§ (ran π βͺ {(π β π)}) βΌ Ο) β βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π ))) |
159 | 140, 158 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β ((π = βͺ (ran π βͺ {(π β π)}) β§ (ran π βͺ {(π β π)}) βΌ Ο) β βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π )) |
160 | 114, 132,
159 | mp2and 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π ) |
161 | | df-rex 3075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ β
(π« (ran π βͺ
{(π β π)}) β© Fin)π = βͺ π β βπ (π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π )) |
162 | | elinel1 4160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β (π« (ran π βͺ {(π β π)}) β© Fin) β π β π« (ran π βͺ {(π β π)})) |
163 | | velpw 4570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β π« (ran π βͺ {(π β π)}) β π β (ran π βͺ {(π β π)})) |
164 | | ssdif 4104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π β (ran π βͺ {(π β π)}) β (π β {(π β π)}) β ((ran π βͺ {(π β π)}) β {(π β π)})) |
165 | | difun2 4445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((ran
π βͺ {(π β π)}) β {(π β π)}) = (ran π β {(π β π)}) |
166 | 164, 165 | sseqtrdi 3999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β (ran π βͺ {(π β π)}) β (π β {(π β π)}) β (ran π β {(π β π)})) |
167 | 166 | difss2d 4099 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β (ran π βͺ {(π β π)}) β (π β {(π β π)}) β ran π) |
168 | 163, 167 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β π« (ran π βͺ {(π β π)}) β (π β {(π β π)}) β ran π) |
169 | 162, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β (π« (ran π βͺ {(π β π)}) β© Fin) β (π β {(π β π)}) β ran π) |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π½ β Top β§ π β π) β (π β (π« (ran π βͺ {(π β π)}) β© Fin) β (π β {(π β π)}) β ran π)) |
171 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π = βͺ
π β (π β π β π β βͺ π )) |
172 | | uniexg 7682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π½ β Top β βͺ π½
β V) |
173 | 1, 172 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π½ β Top β π β V) |
174 | | difexg 5289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π β V β (π β π) β V) |
175 | | unisng 4891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β π) β V β βͺ {(π
β π)} = (π β π)) |
176 | 173, 174,
175 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π½ β Top β βͺ {(π
β π)} = (π β π)) |
177 | 176 | ineq2d 4177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π½ β Top β (π β© βͺ {(π
β π)}) = (π β© (π β π))) |
178 | | disjdif 4436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π β© (π β π)) = β
|
179 | 177, 178 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π½ β Top β (π β© βͺ {(π
β π)}) =
β
) |
180 | | inunissunidif 35875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β© βͺ {(π
β π)}) = β
β (π β βͺ π
β π β βͺ (π
β {(π β π)}))) |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π½ β Top β (π β βͺ π
β π β βͺ (π
β {(π β π)}))) |
182 | 171, 181 | sylan9bbr 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π½ β Top β§ π = βͺ
π ) β (π β π β π β βͺ (π β {(π β π)}))) |
183 | 182 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π½ β Top β§ π = βͺ
π ) β (π β π β π β βͺ (π β {(π β π)}))) |
184 | 183 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π½ β Top β§ π β π) β (π = βͺ π β π β βͺ (π β {(π β π)}))) |
185 | 170, 184 | anim12d 610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π½ β Top β§ π β π) β ((π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)})))) |
186 | 4, 28, 185 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π½ β πΆ β§ π β (Clsdβπ½)) β ((π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)})))) |
187 | 186 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β ((π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)})))) |
188 | 187 | anim2d 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β (((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β§ (π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π )) β ((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β§ ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)}))))) |
189 | 118 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β§ ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)}))) β π β ran π) |
190 | | fvineqsneq 35912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π Fn π β§ βπ β π ((πβπ) β© π) = {π}) β§ ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)}))) β (π β {(π β π)}) = ran π) |
191 | 55, 190 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β§ ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)}))) β (π β {(π β π)}) = ran π) |
192 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ π β V |
193 | | difss 4096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β {(π β π)}) β π |
194 | | ssdomg 8947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β V β ((π β {(π β π)}) β π β (π β {(π β π)}) βΌ π )) |
195 | 192, 193,
194 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β {(π β π)}) βΌ π |
196 | 191, 195 | eqbrtrrdi 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β§ ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)}))) β ran π βΌ π ) |
197 | | endomtr 8959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β ran π β§ ran π βΌ π ) β π βΌ π ) |
198 | 189, 196,
197 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β§ ((π β {(π β π)}) β ran π β§ π β βͺ (π β {(π β π)}))) β π βΌ π ) |
199 | 188, 198 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β (((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β§ (π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π )) β π βΌ π )) |
200 | 199 | expdimp 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β ((π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β π βΌ π )) |
201 | | elinel2 4161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (π« (ran π βͺ {(π β π)}) β© Fin) β π β Fin) |
202 | 201 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β π β Fin) |
203 | 202 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β ((π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β π β Fin)) |
204 | 200, 203 | jcad 514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β ((π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β (π βΌ π β§ π β Fin))) |
205 | 204 | eximdv 1921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β (βπ (π β (π« (ran π βͺ {(π β π)}) β© Fin) β§ π = βͺ π ) β βπ (π βΌ π β§ π β Fin))) |
206 | 161, 205 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β (βπ β (π« (ran π βͺ {(π β π)}) β© Fin)π = βͺ π β βπ (π βΌ π β§ π β Fin))) |
207 | 160, 206 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β§ (π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π})) β βπ (π βΌ π β§ π β Fin)) |
208 | 207 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β ((π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β βπ (π βΌ π β§ π β Fin))) |
209 | 208 | exlimdv 1937 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π½ β πΆ β§ (π β (Clsdβπ½) β§ π β Ο)) β (βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β βπ (π βΌ π β§ π β Fin))) |
210 | 209 | anass1rs 654 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π½ β πΆ β§ π β Ο) β§ π β (Clsdβπ½)) β (βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β βπ (π βΌ π β§ π β Fin))) |
211 | 210 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π½ β πΆ β§ π β Ο) β§ π β (Clsdβπ½) β§ ((limPtβπ½)βπ) = β
) β (βπ(π:πβ1-1βπ½ β§ βπ β π ((πβπ) β© π) = {π}) β βπ (π βΌ π β§ π β Fin))) |
212 | 45, 211 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π½ β πΆ β§ π β Ο) β§ π β (Clsdβπ½) β§ ((limPtβπ½)βπ) = β
) β βπ (π βΌ π β§ π β Fin)) |
213 | 17, 26, 27, 212 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π½ β πΆ β§ π β Ο) β§ π β π) β§ ((limPtβπ½)βπ) = β
) β βπ (π βΌ π β§ π β Fin)) |
214 | 213 | anasss 468 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ ((limPtβπ½)βπ) = β
)) β βπ (π βΌ π β§ π β Fin)) |
215 | | isfinite 9595 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Fin β π βΊ
Ο) |
216 | | domsdomtr 9063 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π βΌ π β§ π βΊ Ο) β π βΊ Ο) |
217 | 215, 216 | sylan2b 595 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π βΌ π β§ π β Fin) β π βΊ Ο) |
218 | 217 | exlimiv 1934 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ (π βΌ π β§ π β Fin) β π βΊ Ο) |
219 | | sdomnen 8928 |
. . . . . . . . . . . . . . . . . . 19
β’ (π βΊ Ο β Β¬
π β
Ο) |
220 | 214, 218,
219 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ ((limPtβπ½)βπ) = β
)) β Β¬ π β Ο) |
221 | 16, 220 | pm2.65da 816 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β πΆ β§ π β Ο) β Β¬ (π β π β§ ((limPtβπ½)βπ) = β
)) |
222 | | imnan 401 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β Β¬ ((limPtβπ½)βπ) = β
) β Β¬ (π β π β§ ((limPtβπ½)βπ) = β
)) |
223 | 221, 222 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β πΆ β§ π β Ο) β (π β π β Β¬ ((limPtβπ½)βπ) = β
)) |
224 | 223 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β Β¬ ((limPtβπ½)βπ) = β
) |
225 | | neq0 4310 |
. . . . . . . . . . . . . . 15
β’ (Β¬
((limPtβπ½)βπ) = β
β βπ π β ((limPtβπ½)βπ)) |
226 | 224, 225 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β βπ π β ((limPtβπ½)βπ)) |
227 | 1 | lpss 22509 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) β π) |
228 | 4, 227 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π½ β πΆ β§ π β π) β ((limPtβπ½)βπ) β π) |
229 | 228 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β ((limPtβπ½)βπ) β π) |
230 | 229 | sseld 3948 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β (π β ((limPtβπ½)βπ) β π β π)) |
231 | 230 | ancrd 553 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β (π β ((limPtβπ½)βπ) β (π β π β§ π β ((limPtβπ½)βπ)))) |
232 | 231 | eximdv 1921 |
. . . . . . . . . . . . . . 15
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β (βπ π β ((limPtβπ½)βπ) β βπ (π β π β§ π β ((limPtβπ½)βπ)))) |
233 | | df-rex 3075 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π π β ((limPtβπ½)βπ) β βπ (π β π β§ π β ((limPtβπ½)βπ))) |
234 | 232, 233 | syl6ibr 252 |
. . . . . . . . . . . . . 14
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β (βπ π β ((limPtβπ½)βπ) β βπ β π π β ((limPtβπ½)βπ))) |
235 | 226, 234 | mpd 15 |
. . . . . . . . . . . . 13
β’ (((π½ β πΆ β§ π β Ο) β§ π β π) β βπ β π π β ((limPtβπ½)βπ)) |
236 | 15, 235 | sylan2 594 |
. . . . . . . . . . . 12
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ π β π)) β βπ β π π β ((limPtβπ½)βπ)) |
237 | 1 | lpss3 22511 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π β π β§ π β π) β ((limPtβπ½)βπ) β ((limPtβπ½)βπ)) |
238 | 237 | 3expb 1121 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ (π β π β§ π β π)) β ((limPtβπ½)βπ) β ((limPtβπ½)βπ)) |
239 | 4, 238 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((π½ β πΆ β§ (π β π β§ π β π)) β ((limPtβπ½)βπ) β ((limPtβπ½)βπ)) |
240 | 239 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ π β π)) β ((limPtβπ½)βπ) β ((limPtβπ½)βπ)) |
241 | 240 | sseld 3948 |
. . . . . . . . . . . . 13
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ π β π)) β (π β ((limPtβπ½)βπ) β π β ((limPtβπ½)βπ))) |
242 | 241 | reximdv 3168 |
. . . . . . . . . . . 12
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ π β π)) β (βπ β π π β ((limPtβπ½)βπ) β βπ β π π β ((limPtβπ½)βπ))) |
243 | 236, 242 | mpd 15 |
. . . . . . . . . . 11
β’ (((π½ β πΆ β§ π β Ο) β§ (π β π β§ π β π)) β βπ β π π β ((limPtβπ½)βπ)) |
244 | 243 | an42s 660 |
. . . . . . . . . 10
β’ (((π½ β πΆ β§ π β π) β§ (π β π β§ π β Ο)) β βπ β π π β ((limPtβπ½)βπ)) |
245 | 244 | ex 414 |
. . . . . . . . 9
β’ ((π½ β πΆ β§ π β π) β ((π β π β§ π β Ο) β βπ β π π β ((limPtβπ½)βπ))) |
246 | 245 | exlimdv 1937 |
. . . . . . . 8
β’ ((π½ β πΆ β§ π β π) β (βπ(π β π β§ π β Ο) β βπ β π π β ((limPtβπ½)βπ))) |
247 | 246 | adantrr 716 |
. . . . . . 7
β’ ((π½ β πΆ β§ (π β π β§ Β¬ π β Fin)) β (βπ(π β π β§ π β Ο) β βπ β π π β ((limPtβπ½)βπ))) |
248 | 13, 247 | mpd 15 |
. . . . . 6
β’ ((π½ β πΆ β§ (π β π β§ Β¬ π β Fin)) β βπ β π π β ((limPtβπ½)βπ)) |
249 | 7, 248 | sylan2b 595 |
. . . . 5
β’ ((π½ β πΆ β§ (π β π« π β§ Β¬ π β Fin)) β βπ β π π β ((limPtβπ½)βπ)) |
250 | 5, 249 | sylan2b 595 |
. . . 4
β’ ((π½ β πΆ β§ π β (π« π β Fin)) β βπ β π π β ((limPtβπ½)βπ)) |
251 | 250 | ralrimiva 3144 |
. . 3
β’ (π½ β πΆ β βπ β (π« π β Fin)βπ β π π β ((limPtβπ½)βπ)) |
252 | | simpr 486 |
. . . . . 6
β’ ((π¦ = π β§ π§ = π ) β π§ = π ) |
253 | | fveq2 6847 |
. . . . . . 7
β’ (π¦ = π β ((limPtβπ½)βπ¦) = ((limPtβπ½)βπ)) |
254 | 253 | adantr 482 |
. . . . . 6
β’ ((π¦ = π β§ π§ = π ) β ((limPtβπ½)βπ¦) = ((limPtβπ½)βπ)) |
255 | 252, 254 | eleq12d 2832 |
. . . . 5
β’ ((π¦ = π β§ π§ = π ) β (π§ β ((limPtβπ½)βπ¦) β π β ((limPtβπ½)βπ))) |
256 | 255 | cbvrexdva 3330 |
. . . 4
β’ (π¦ = π β (βπ§ β π π§ β ((limPtβπ½)βπ¦) β βπ β π π β ((limPtβπ½)βπ))) |
257 | 256 | cbvralvw 3228 |
. . 3
β’
(βπ¦ β
(π« π β
Fin)βπ§ β π π§ β ((limPtβπ½)βπ¦) β βπ β (π« π β Fin)βπ β π π β ((limPtβπ½)βπ)) |
258 | 251, 257 | sylibr 233 |
. 2
β’ (π½ β πΆ β βπ¦ β (π« π β Fin)βπ§ β π π§ β ((limPtβπ½)βπ¦)) |
259 | | pibt2.21 |
. . 3
β’ π = {π₯ β Top β£ βπ¦ β (π« βͺ π₯
β Fin)βπ§ β
βͺ π₯π§ β ((limPtβπ₯)βπ¦)} |
260 | 1, 259 | pibp21 35915 |
. 2
β’ (π½ β π β (π½ β Top β§ βπ¦ β (π« π β Fin)βπ§ β π π§ β ((limPtβπ½)βπ¦))) |
261 | 4, 258, 260 | sylanbrc 584 |
1
β’ (π½ β πΆ β π½ β π) |