Step | Hyp | Ref
| Expression |
1 | | pm3.24 404 |
. . . . . . 7
β’ Β¬
((π΄ β© π) β Fin β§ Β¬ (π΄ β© π) β Fin) |
2 | 1 | a1i 11 |
. . . . . 6
β’ (π β π§ β Β¬ ((π΄ β© π) β Fin β§ Β¬ (π΄ β© π) β Fin)) |
3 | 2 | nrex 3078 |
. . . . 5
β’ Β¬
βπ β π§ ((π΄ β© π) β Fin β§ Β¬ (π΄ β© π) β Fin) |
4 | | r19.29 3118 |
. . . . 5
β’
((βπ β
π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin) β βπ β π§ ((π΄ β© π) β Fin β§ Β¬ (π΄ β© π) β Fin)) |
5 | 3, 4 | mto 196 |
. . . 4
β’ Β¬
(βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin) |
6 | 5 | a1i 11 |
. . 3
β’ (π§ β (π« π½ β© Fin) β Β¬
(βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin)) |
7 | 6 | nrex 3078 |
. 2
β’ Β¬
βπ§ β (π«
π½ β© Fin)(βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin) |
8 | | ralnex 3076 |
. . . . . 6
β’
(βπ₯ β
π Β¬ π₯ β ((limPtβπ½)βπ΄) β Β¬ βπ₯ β π π₯ β ((limPtβπ½)βπ΄)) |
9 | | cmptop 22762 |
. . . . . . 7
β’ (π½ β Comp β π½ β Top) |
10 | | bwt2.1 |
. . . . . . . . . . 11
β’ π = βͺ
π½ |
11 | 10 | islp3 22513 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π΄ β π β§ π₯ β π) β (π₯ β ((limPtβπ½)βπ΄) β βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
))) |
12 | 11 | 3expa 1119 |
. . . . . . . . 9
β’ (((π½ β Top β§ π΄ β π) β§ π₯ β π) β (π₯ β ((limPtβπ½)βπ΄) β βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
))) |
13 | 12 | notbid 318 |
. . . . . . . 8
β’ (((π½ β Top β§ π΄ β π) β§ π₯ β π) β (Β¬ π₯ β ((limPtβπ½)βπ΄) β Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
))) |
14 | 13 | ralbidva 3173 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β π) β (βπ₯ β π Β¬ π₯ β ((limPtβπ½)βπ΄) β βπ₯ β π Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
))) |
15 | 9, 14 | sylan 581 |
. . . . . 6
β’ ((π½ β Comp β§ π΄ β π) β (βπ₯ β π Β¬ π₯ β ((limPtβπ½)βπ΄) β βπ₯ β π Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
))) |
16 | 8, 15 | bitr3id 285 |
. . . . 5
β’ ((π½ β Comp β§ π΄ β π) β (Β¬ βπ₯ β π π₯ β ((limPtβπ½)βπ΄) β βπ₯ β π Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
))) |
17 | | rexanali 3106 |
. . . . . . . . 9
β’
(βπ β
π½ (π₯ β π β§ Β¬ (π β© (π΄ β {π₯})) β β
) β Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
)) |
18 | | nne 2948 |
. . . . . . . . . . . 12
β’ (Β¬
(π β© (π΄ β {π₯})) β β
β (π β© (π΄ β {π₯})) = β
) |
19 | | vex 3452 |
. . . . . . . . . . . . 13
β’ π₯ β V |
20 | | sneq 4601 |
. . . . . . . . . . . . . . . 16
β’ (π = π₯ β {π} = {π₯}) |
21 | 20 | difeq2d 4087 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (π΄ β {π}) = (π΄ β {π₯})) |
22 | 21 | ineq2d 4177 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (π β© (π΄ β {π})) = (π β© (π΄ β {π₯}))) |
23 | 22 | eqeq1d 2739 |
. . . . . . . . . . . . 13
β’ (π = π₯ β ((π β© (π΄ β {π})) = β
β (π β© (π΄ β {π₯})) = β
)) |
24 | 19, 23 | spcev 3568 |
. . . . . . . . . . . 12
β’ ((π β© (π΄ β {π₯})) = β
β βπ(π β© (π΄ β {π})) = β
) |
25 | 18, 24 | sylbi 216 |
. . . . . . . . . . 11
β’ (Β¬
(π β© (π΄ β {π₯})) β β
β βπ(π β© (π΄ β {π})) = β
) |
26 | 25 | anim2i 618 |
. . . . . . . . . 10
β’ ((π₯ β π β§ Β¬ (π β© (π΄ β {π₯})) β β
) β (π₯ β π β§ βπ(π β© (π΄ β {π})) = β
)) |
27 | 26 | reximi 3088 |
. . . . . . . . 9
β’
(βπ β
π½ (π₯ β π β§ Β¬ (π β© (π΄ β {π₯})) β β
) β βπ β π½ (π₯ β π β§ βπ(π β© (π΄ β {π})) = β
)) |
28 | 17, 27 | sylbir 234 |
. . . . . . . 8
β’ (Β¬
βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
) β βπ β π½ (π₯ β π β§ βπ(π β© (π΄ β {π})) = β
)) |
29 | 28 | ralimi 3087 |
. . . . . . 7
β’
(βπ₯ β
π Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
) β βπ₯ β π βπ β π½ (π₯ β π β§ βπ(π β© (π΄ β {π})) = β
)) |
30 | 10 | cmpcov2 22757 |
. . . . . . . 8
β’ ((π½ β Comp β§ βπ₯ β π βπ β π½ (π₯ β π β§ βπ(π β© (π΄ β {π})) = β
)) β βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
)) |
31 | 30 | ex 414 |
. . . . . . 7
β’ (π½ β Comp β
(βπ₯ β π βπ β π½ (π₯ β π β§ βπ(π β© (π΄ β {π})) = β
) β βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
))) |
32 | 29, 31 | syl5 34 |
. . . . . 6
β’ (π½ β Comp β
(βπ₯ β π Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
) β βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
))) |
33 | 32 | adantr 482 |
. . . . 5
β’ ((π½ β Comp β§ π΄ β π) β (βπ₯ β π Β¬ βπ β π½ (π₯ β π β (π β© (π΄ β {π₯})) β β
) β βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
))) |
34 | 16, 33 | sylbid 239 |
. . . 4
β’ ((π½ β Comp β§ π΄ β π) β (Β¬ βπ₯ β π π₯ β ((limPtβπ½)βπ΄) β βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
))) |
35 | 34 | 3adant3 1133 |
. . 3
β’ ((π½ β Comp β§ π΄ β π β§ Β¬ π΄ β Fin) β (Β¬ βπ₯ β π π₯ β ((limPtβπ½)βπ΄) β βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
))) |
36 | | elinel2 4161 |
. . . . . . . 8
β’ (π§ β (π« π½ β© Fin) β π§ β Fin) |
37 | | sseq2 3975 |
. . . . . . . . . . . 12
β’ (π = βͺ
π§ β (π΄ β π β π΄ β βͺ π§)) |
38 | 37 | biimpac 480 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ π = βͺ π§) β π΄ β βͺ π§) |
39 | | infssuni 9294 |
. . . . . . . . . . . . 13
β’ ((Β¬
π΄ β Fin β§ π§ β Fin β§ π΄ β βͺ π§)
β βπ β
π§ Β¬ (π΄ β© π) β Fin) |
40 | 39 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((Β¬
π΄ β Fin β§ π§ β Fin) β§ π΄ β βͺ π§)
β βπ β
π§ Β¬ (π΄ β© π) β Fin) |
41 | 40 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π΄ β βͺ π§
β§ (Β¬ π΄ β Fin
β§ π§ β Fin)) β
βπ β π§ Β¬ (π΄ β© π) β Fin) |
42 | 38, 41 | sylan 581 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π = βͺ π§) β§ (Β¬ π΄ β Fin β§ π§ β Fin)) β βπ β π§ Β¬ (π΄ β© π) β Fin) |
43 | 42 | an42s 660 |
. . . . . . . . 9
β’ (((π΄ β π β§ Β¬ π΄ β Fin) β§ (π§ β Fin β§ π = βͺ π§)) β βπ β π§ Β¬ (π΄ β© π) β Fin) |
44 | 43 | anassrs 469 |
. . . . . . . 8
β’ ((((π΄ β π β§ Β¬ π΄ β Fin) β§ π§ β Fin) β§ π = βͺ π§) β βπ β π§ Β¬ (π΄ β© π) β Fin) |
45 | 36, 44 | sylanl2 680 |
. . . . . . 7
β’ ((((π΄ β π β§ Β¬ π΄ β Fin) β§ π§ β (π« π½ β© Fin)) β§ π = βͺ π§) β βπ β π§ Β¬ (π΄ β© π) β Fin) |
46 | | 0fin 9122 |
. . . . . . . . . . . 12
β’ β
β Fin |
47 | | eleq1 2826 |
. . . . . . . . . . . 12
β’ ((π β© (π΄ β {π})) = β
β ((π β© (π΄ β {π})) β Fin β β
β
Fin)) |
48 | 46, 47 | mpbiri 258 |
. . . . . . . . . . 11
β’ ((π β© (π΄ β {π})) = β
β (π β© (π΄ β {π})) β Fin) |
49 | | snfi 8995 |
. . . . . . . . . . 11
β’ {π} β Fin |
50 | | unfi 9123 |
. . . . . . . . . . 11
β’ (((π β© (π΄ β {π})) β Fin β§ {π} β Fin) β ((π β© (π΄ β {π})) βͺ {π}) β Fin) |
51 | 48, 49, 50 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β© (π΄ β {π})) = β
β ((π β© (π΄ β {π})) βͺ {π}) β Fin) |
52 | | ssun1 4137 |
. . . . . . . . . . . 12
β’ π β (π βͺ {π}) |
53 | | ssun1 4137 |
. . . . . . . . . . . . 13
β’ π΄ β (π΄ βͺ {π}) |
54 | | undif1 4440 |
. . . . . . . . . . . . 13
β’ ((π΄ β {π}) βͺ {π}) = (π΄ βͺ {π}) |
55 | 53, 54 | sseqtrri 3986 |
. . . . . . . . . . . 12
β’ π΄ β ((π΄ β {π}) βͺ {π}) |
56 | | ss2in 4201 |
. . . . . . . . . . . 12
β’ ((π β (π βͺ {π}) β§ π΄ β ((π΄ β {π}) βͺ {π})) β (π β© π΄) β ((π βͺ {π}) β© ((π΄ β {π}) βͺ {π}))) |
57 | 52, 55, 56 | mp2an 691 |
. . . . . . . . . . 11
β’ (π β© π΄) β ((π βͺ {π}) β© ((π΄ β {π}) βͺ {π})) |
58 | | incom 4166 |
. . . . . . . . . . 11
β’ (π΄ β© π) = (π β© π΄) |
59 | | undir 4241 |
. . . . . . . . . . 11
β’ ((π β© (π΄ β {π})) βͺ {π}) = ((π βͺ {π}) β© ((π΄ β {π}) βͺ {π})) |
60 | 57, 58, 59 | 3sstr4i 3992 |
. . . . . . . . . 10
β’ (π΄ β© π) β ((π β© (π΄ β {π})) βͺ {π}) |
61 | | ssfi 9124 |
. . . . . . . . . 10
β’ ((((π β© (π΄ β {π})) βͺ {π}) β Fin β§ (π΄ β© π) β ((π β© (π΄ β {π})) βͺ {π})) β (π΄ β© π) β Fin) |
62 | 51, 60, 61 | sylancl 587 |
. . . . . . . . 9
β’ ((π β© (π΄ β {π})) = β
β (π΄ β© π) β Fin) |
63 | 62 | exlimiv 1934 |
. . . . . . . 8
β’
(βπ(π β© (π΄ β {π})) = β
β (π΄ β© π) β Fin) |
64 | 63 | ralimi 3087 |
. . . . . . 7
β’
(βπ β
π§ βπ(π β© (π΄ β {π})) = β
β βπ β π§ (π΄ β© π) β Fin) |
65 | 45, 64 | anim12ci 615 |
. . . . . 6
β’
(((((π΄ β π β§ Β¬ π΄ β Fin) β§ π§ β (π« π½ β© Fin)) β§ π = βͺ π§) β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
) β (βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin)) |
66 | 65 | expl 459 |
. . . . 5
β’ (((π΄ β π β§ Β¬ π΄ β Fin) β§ π§ β (π« π½ β© Fin)) β ((π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
) β (βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin))) |
67 | 66 | reximdva 3166 |
. . . 4
β’ ((π΄ β π β§ Β¬ π΄ β Fin) β (βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
) β βπ§ β (π« π½ β© Fin)(βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin))) |
68 | 67 | 3adant1 1131 |
. . 3
β’ ((π½ β Comp β§ π΄ β π β§ Β¬ π΄ β Fin) β (βπ§ β (π« π½ β© Fin)(π = βͺ π§ β§ βπ β π§ βπ(π β© (π΄ β {π})) = β
) β βπ§ β (π« π½ β© Fin)(βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin))) |
69 | 35, 68 | syld 47 |
. 2
β’ ((π½ β Comp β§ π΄ β π β§ Β¬ π΄ β Fin) β (Β¬ βπ₯ β π π₯ β ((limPtβπ½)βπ΄) β βπ§ β (π« π½ β© Fin)(βπ β π§ (π΄ β© π) β Fin β§ βπ β π§ Β¬ (π΄ β© π) β Fin))) |
70 | 7, 69 | mt3i 149 |
1
β’ ((π½ β Comp β§ π΄ β π β§ Β¬ π΄ β Fin) β βπ₯ β π π₯ β ((limPtβπ½)βπ΄)) |