Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²π’ Β¬ π΄ β Fin |
2 | | nfab1 2910 |
. . . . 5
β’
β²π’{π’ β£ βπ¦ β π΄ π’ = {π¦}} |
3 | | nfcv 2908 |
. . . . 5
β’
β²π’π |
4 | | abid 2718 |
. . . . . . . . . . 11
β’ (π’ β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β βπ¦ β π΄ π’ = {π¦}) |
5 | | df-rex 3075 |
. . . . . . . . . . 11
β’
(βπ¦ β
π΄ π’ = {π¦} β βπ¦(π¦ β π΄ β§ π’ = {π¦})) |
6 | 4, 5 | bitri 275 |
. . . . . . . . . 10
β’ (π’ β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β βπ¦(π¦ β π΄ β§ π’ = {π¦})) |
7 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ {π¦} = {π¦} |
8 | | vsnex 5391 |
. . . . . . . . . . . . . . . . . 18
β’ {π¦} β V |
9 | | snelpwi 5405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β π΄ β {π¦} β π« π΄) |
10 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ = {π¦} β (π₯ β π« π΄ β {π¦} β π« π΄)) |
11 | 9, 10 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = {π¦} β (π¦ β π΄ β π₯ β π« π΄)) |
12 | 11 | imdistani 570 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ = {π¦} β§ π¦ β π΄) β (π₯ = {π¦} β§ π₯ β π« π΄)) |
13 | 12 | anim2i 618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((Β¬
π΄ β Fin β§ (π₯ = {π¦} β§ π¦ β π΄)) β (Β¬ π΄ β Fin β§ (π₯ = {π¦} β§ π₯ β π« π΄))) |
14 | 13 | 3impb 1116 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β (Β¬ π΄ β Fin β§ (π₯ = {π¦} β§ π₯ β π« π΄))) |
15 | | 3anass 1096 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π₯ β π« π΄) β (Β¬ π΄ β Fin β§ (π₯ = {π¦} β§ π₯ β π« π΄))) |
16 | 14, 15 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β (Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π₯ β π« π΄)) |
17 | | snfi 8995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ {π¦} β Fin |
18 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ = {π¦} β (π₯ β Fin β {π¦} β Fin)) |
19 | 17, 18 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ = {π¦} β π₯ β Fin) |
20 | | difinf 9267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((Β¬
π΄ β Fin β§ π₯ β Fin) β Β¬ (π΄ β π₯) β Fin) |
21 | 19, 20 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦}) β Β¬ (π΄ β π₯) β Fin) |
22 | 21 | orcd 872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦}) β (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄))) |
23 | 22 | anim2i 618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π₯ β π« π΄ β§ (Β¬ π΄ β Fin β§ π₯ = {π¦})) β (π₯ β π« π΄ β§ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄)))) |
24 | 23 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((Β¬
π΄ β Fin β§ π₯ = {π¦}) β§ π₯ β π« π΄) β (π₯ β π« π΄ β§ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄)))) |
25 | 24 | 3impa 1111 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π₯ β π« π΄) β (π₯ β π« π΄ β§ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄)))) |
26 | 16, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β (π₯ β π« π΄ β§ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄)))) |
27 | | topdifinf.t |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄))} |
28 | 27 | reqabi 3432 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β π β (π₯ β π« π΄ β§ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄)))) |
29 | 26, 28 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β π₯ β π) |
30 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = {π¦} β (π₯ β π β {π¦} β π)) |
31 | 30 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β (π₯ β π β {π¦} β π)) |
32 | 29, 31 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Β¬
π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β {π¦} β π) |
33 | 32 | sbcth 3759 |
. . . . . . . . . . . . . . . . . 18
β’ ({π¦} β V β [{π¦} / π₯]((Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β {π¦} β π)) |
34 | 8, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
[{π¦} / π₯]((Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β {π¦} β π) |
35 | | sbcimg 3795 |
. . . . . . . . . . . . . . . . . 18
β’ ({π¦} β V β
([{π¦} / π₯]((Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β {π¦} β π) β ([{π¦} / π₯](Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β [{π¦} / π₯]{π¦} β π))) |
36 | 8, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
([{π¦} / π₯]((Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β {π¦} β π) β ([{π¦} / π₯](Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β [{π¦} / π₯]{π¦} β π)) |
37 | 34, 36 | mpbi 229 |
. . . . . . . . . . . . . . . 16
β’
([{π¦} / π₯](Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β [{π¦} / π₯]{π¦} β π) |
38 | | sbc3an 3814 |
. . . . . . . . . . . . . . . . . 18
β’
([{π¦} / π₯](Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β ([{π¦} / π₯] Β¬ π΄ β Fin β§ [{π¦} / π₯]π₯ = {π¦} β§ [{π¦} / π₯]π¦ β π΄)) |
39 | | sbcg 3823 |
. . . . . . . . . . . . . . . . . . . 20
β’ ({π¦} β V β
([{π¦} / π₯] Β¬ π΄ β Fin β Β¬ π΄ β Fin)) |
40 | 8, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’
([{π¦} / π₯] Β¬ π΄ β Fin β Β¬ π΄ β Fin) |
41 | 40 | 3anbi1i 1158 |
. . . . . . . . . . . . . . . . . 18
β’
(([{π¦} /
π₯] Β¬ π΄ β Fin β§ [{π¦} / π₯]π₯ = {π¦} β§ [{π¦} / π₯]π¦ β π΄) β (Β¬ π΄ β Fin β§ [{π¦} / π₯]π₯ = {π¦} β§ [{π¦} / π₯]π¦ β π΄)) |
42 | | eqsbc1 3793 |
. . . . . . . . . . . . . . . . . . . 20
β’ ({π¦} β V β
([{π¦} / π₯]π₯ = {π¦} β {π¦} = {π¦})) |
43 | 8, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’
([{π¦} / π₯]π₯ = {π¦} β {π¦} = {π¦}) |
44 | 43 | 3anbi2i 1159 |
. . . . . . . . . . . . . . . . . 18
β’ ((Β¬
π΄ β Fin β§
[{π¦} / π₯]π₯ = {π¦} β§ [{π¦} / π₯]π¦ β π΄) β (Β¬ π΄ β Fin β§ {π¦} = {π¦} β§ [{π¦} / π₯]π¦ β π΄)) |
45 | 38, 41, 44 | 3bitri 297 |
. . . . . . . . . . . . . . . . 17
β’
([{π¦} / π₯](Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β (Β¬ π΄ β Fin β§ {π¦} = {π¦} β§ [{π¦} / π₯]π¦ β π΄)) |
46 | | sbcg 3823 |
. . . . . . . . . . . . . . . . . . 19
β’ ({π¦} β V β
([{π¦} / π₯]π¦ β π΄ β π¦ β π΄)) |
47 | 8, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
([{π¦} / π₯]π¦ β π΄ β π¦ β π΄) |
48 | 47 | 3anbi3i 1160 |
. . . . . . . . . . . . . . . . 17
β’ ((Β¬
π΄ β Fin β§ {π¦} = {π¦} β§ [{π¦} / π₯]π¦ β π΄) β (Β¬ π΄ β Fin β§ {π¦} = {π¦} β§ π¦ β π΄)) |
49 | 45, 48 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’
([{π¦} / π₯](Β¬ π΄ β Fin β§ π₯ = {π¦} β§ π¦ β π΄) β (Β¬ π΄ β Fin β§ {π¦} = {π¦} β§ π¦ β π΄)) |
50 | | sbcg 3823 |
. . . . . . . . . . . . . . . . 17
β’ ({π¦} β V β
([{π¦} / π₯]{π¦} β π β {π¦} β π)) |
51 | 8, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
([{π¦} / π₯]{π¦} β π β {π¦} β π) |
52 | 37, 49, 51 | 3imtr3i 291 |
. . . . . . . . . . . . . . 15
β’ ((Β¬
π΄ β Fin β§ {π¦} = {π¦} β§ π¦ β π΄) β {π¦} β π) |
53 | 7, 52 | mp3an2 1450 |
. . . . . . . . . . . . . 14
β’ ((Β¬
π΄ β Fin β§ π¦ β π΄) β {π¦} β π) |
54 | 53 | ex 414 |
. . . . . . . . . . . . 13
β’ (Β¬
π΄ β Fin β (π¦ β π΄ β {π¦} β π)) |
55 | 54 | pm4.71d 563 |
. . . . . . . . . . . 12
β’ (Β¬
π΄ β Fin β (π¦ β π΄ β (π¦ β π΄ β§ {π¦} β π))) |
56 | 55 | anbi1d 631 |
. . . . . . . . . . 11
β’ (Β¬
π΄ β Fin β ((π¦ β π΄ β§ π’ = {π¦}) β ((π¦ β π΄ β§ {π¦} β π) β§ π’ = {π¦}))) |
57 | 56 | exbidv 1925 |
. . . . . . . . . 10
β’ (Β¬
π΄ β Fin β
(βπ¦(π¦ β π΄ β§ π’ = {π¦}) β βπ¦((π¦ β π΄ β§ {π¦} β π) β§ π’ = {π¦}))) |
58 | 6, 57 | bitrid 283 |
. . . . . . . . 9
β’ (Β¬
π΄ β Fin β (π’ β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β βπ¦((π¦ β π΄ β§ {π¦} β π) β§ π’ = {π¦}))) |
59 | | anass 470 |
. . . . . . . . . . 11
β’ (((π¦ β π΄ β§ {π¦} β π) β§ π’ = {π¦}) β (π¦ β π΄ β§ ({π¦} β π β§ π’ = {π¦}))) |
60 | 59 | exbii 1851 |
. . . . . . . . . 10
β’
(βπ¦((π¦ β π΄ β§ {π¦} β π) β§ π’ = {π¦}) β βπ¦(π¦ β π΄ β§ ({π¦} β π β§ π’ = {π¦}))) |
61 | | exsimpr 1873 |
. . . . . . . . . 10
β’
(βπ¦(π¦ β π΄ β§ ({π¦} β π β§ π’ = {π¦})) β βπ¦({π¦} β π β§ π’ = {π¦})) |
62 | 60, 61 | sylbi 216 |
. . . . . . . . 9
β’
(βπ¦((π¦ β π΄ β§ {π¦} β π) β§ π’ = {π¦}) β βπ¦({π¦} β π β§ π’ = {π¦})) |
63 | 58, 62 | syl6bi 253 |
. . . . . . . 8
β’ (Β¬
π΄ β Fin β (π’ β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β βπ¦({π¦} β π β§ π’ = {π¦}))) |
64 | | ancom 462 |
. . . . . . . . . 10
β’ (({π¦} β π β§ π’ = {π¦}) β (π’ = {π¦} β§ {π¦} β π)) |
65 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π’ = {π¦} β (π’ β π β {π¦} β π)) |
66 | 65 | pm5.32i 576 |
. . . . . . . . . 10
β’ ((π’ = {π¦} β§ π’ β π) β (π’ = {π¦} β§ {π¦} β π)) |
67 | 64, 66 | bitr4i 278 |
. . . . . . . . 9
β’ (({π¦} β π β§ π’ = {π¦}) β (π’ = {π¦} β§ π’ β π)) |
68 | 67 | exbii 1851 |
. . . . . . . 8
β’
(βπ¦({π¦} β π β§ π’ = {π¦}) β βπ¦(π’ = {π¦} β§ π’ β π)) |
69 | 63, 68 | syl6ib 251 |
. . . . . . 7
β’ (Β¬
π΄ β Fin β (π’ β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β βπ¦(π’ = {π¦} β§ π’ β π))) |
70 | | exsimpr 1873 |
. . . . . . 7
β’
(βπ¦(π’ = {π¦} β§ π’ β π) β βπ¦ π’ β π) |
71 | 69, 70 | syl6 35 |
. . . . . 6
β’ (Β¬
π΄ β Fin β (π’ β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β βπ¦ π’ β π)) |
72 | | ax5e 1916 |
. . . . . 6
β’
(βπ¦ π’ β π β π’ β π) |
73 | 71, 72 | syl6 35 |
. . . . 5
β’ (Β¬
π΄ β Fin β (π’ β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β π’ β π)) |
74 | 1, 2, 3, 73 | ssrd 3954 |
. . . 4
β’ (Β¬
π΄ β Fin β {π’ β£ βπ¦ β π΄ π’ = {π¦}} β π) |
75 | | eqid 2737 |
. . . . 5
β’ {π’ β£ βπ¦ β π΄ π’ = {π¦}} = {π’ β£ βπ¦ β π΄ π’ = {π¦}} |
76 | 75 | dissneq 35841 |
. . . 4
β’ (({π’ β£ βπ¦ β π΄ π’ = {π¦}} β π β§ π β (TopOnβπ΄)) β π = π« π΄) |
77 | 74, 76 | sylan 581 |
. . 3
β’ ((Β¬
π΄ β Fin β§ π β (TopOnβπ΄)) β π = π« π΄) |
78 | | nfielex 9224 |
. . . . 5
β’ (Β¬
π΄ β Fin β
βπ¦ π¦ β π΄) |
79 | 78 | adantr 482 |
. . . 4
β’ ((Β¬
π΄ β Fin β§ π β (TopOnβπ΄)) β βπ¦ π¦ β π΄) |
80 | | difss 4096 |
. . . . . . 7
β’ (π΄ β {π¦}) β π΄ |
81 | | elfvex 6885 |
. . . . . . . 8
β’ (π β (TopOnβπ΄) β π΄ β V) |
82 | | difexg 5289 |
. . . . . . . 8
β’ (π΄ β V β (π΄ β {π¦}) β V) |
83 | | elpwg 4568 |
. . . . . . . 8
β’ ((π΄ β {π¦}) β V β ((π΄ β {π¦}) β π« π΄ β (π΄ β {π¦}) β π΄)) |
84 | 81, 82, 83 | 3syl 18 |
. . . . . . 7
β’ (π β (TopOnβπ΄) β ((π΄ β {π¦}) β π« π΄ β (π΄ β {π¦}) β π΄)) |
85 | 80, 84 | mpbiri 258 |
. . . . . 6
β’ (π β (TopOnβπ΄) β (π΄ β {π¦}) β π« π΄) |
86 | 85 | adantl 483 |
. . . . 5
β’ ((Β¬
π΄ β Fin β§ π β (TopOnβπ΄)) β (π΄ β {π¦}) β π« π΄) |
87 | | difinf 9267 |
. . . . . . . . . . . 12
β’ ((Β¬
π΄ β Fin β§ {π¦} β Fin) β Β¬
(π΄ β {π¦}) β Fin) |
88 | 17, 87 | mpan2 690 |
. . . . . . . . . . 11
β’ (Β¬
π΄ β Fin β Β¬
(π΄ β {π¦}) β Fin) |
89 | | 0fin 9122 |
. . . . . . . . . . . 12
β’ β
β Fin |
90 | | eleq1 2826 |
. . . . . . . . . . . 12
β’ ((π΄ β {π¦}) = β
β ((π΄ β {π¦}) β Fin β β
β
Fin)) |
91 | 89, 90 | mpbiri 258 |
. . . . . . . . . . 11
β’ ((π΄ β {π¦}) = β
β (π΄ β {π¦}) β Fin) |
92 | 88, 91 | nsyl 140 |
. . . . . . . . . 10
β’ (Β¬
π΄ β Fin β Β¬
(π΄ β {π¦}) = β
) |
93 | 92 | ad2antrl 727 |
. . . . . . . . 9
β’ ((π¦ β π΄ β§ (Β¬ π΄ β Fin β§ π β (TopOnβπ΄))) β Β¬ (π΄ β {π¦}) = β
) |
94 | | vsnid 4628 |
. . . . . . . . . . . . . 14
β’ π¦ β {π¦} |
95 | | inelcm 4429 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π΄ β§ π¦ β {π¦}) β (π΄ β© {π¦}) β β
) |
96 | 94, 95 | mpan2 690 |
. . . . . . . . . . . . 13
β’ (π¦ β π΄ β (π΄ β© {π¦}) β β
) |
97 | | disj4 4423 |
. . . . . . . . . . . . . 14
β’ ((π΄ β© {π¦}) = β
β Β¬ (π΄ β {π¦}) β π΄) |
98 | 97 | necon2abii 2995 |
. . . . . . . . . . . . 13
β’ ((π΄ β {π¦}) β π΄ β (π΄ β© {π¦}) β β
) |
99 | 96, 98 | sylibr 233 |
. . . . . . . . . . . 12
β’ (π¦ β π΄ β (π΄ β {π¦}) β π΄) |
100 | 99 | pssned 4063 |
. . . . . . . . . . 11
β’ (π¦ β π΄ β (π΄ β {π¦}) β π΄) |
101 | 100 | adantr 482 |
. . . . . . . . . 10
β’ ((π¦ β π΄ β§ (Β¬ π΄ β Fin β§ π β (TopOnβπ΄))) β (π΄ β {π¦}) β π΄) |
102 | 101 | neneqd 2949 |
. . . . . . . . 9
β’ ((π¦ β π΄ β§ (Β¬ π΄ β Fin β§ π β (TopOnβπ΄))) β Β¬ (π΄ β {π¦}) = π΄) |
103 | 93, 102 | jca 513 |
. . . . . . . 8
β’ ((π¦ β π΄ β§ (Β¬ π΄ β Fin β§ π β (TopOnβπ΄))) β (Β¬ (π΄ β {π¦}) = β
β§ Β¬ (π΄ β {π¦}) = π΄)) |
104 | | pm4.56 988 |
. . . . . . . 8
β’ ((Β¬
(π΄ β {π¦}) = β
β§ Β¬ (π΄ β {π¦}) = π΄) β Β¬ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄)) |
105 | 103, 104 | sylib 217 |
. . . . . . 7
β’ ((π¦ β π΄ β§ (Β¬ π΄ β Fin β§ π β (TopOnβπ΄))) β Β¬ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄)) |
106 | | difeq2 4081 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π΄ β {π¦}) β (π΄ β π₯) = (π΄ β (π΄ β {π¦}))) |
107 | 106 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π₯ = (π΄ β {π¦}) β ((π΄ β π₯) β Fin β (π΄ β (π΄ β {π¦})) β Fin)) |
108 | 107 | notbid 318 |
. . . . . . . . . . . 12
β’ (π₯ = (π΄ β {π¦}) β (Β¬ (π΄ β π₯) β Fin β Β¬ (π΄ β (π΄ β {π¦})) β Fin)) |
109 | | eqeq1 2741 |
. . . . . . . . . . . . 13
β’ (π₯ = (π΄ β {π¦}) β (π₯ = β
β (π΄ β {π¦}) = β
)) |
110 | | eqeq1 2741 |
. . . . . . . . . . . . 13
β’ (π₯ = (π΄ β {π¦}) β (π₯ = π΄ β (π΄ β {π¦}) = π΄)) |
111 | 109, 110 | orbi12d 918 |
. . . . . . . . . . . 12
β’ (π₯ = (π΄ β {π¦}) β ((π₯ = β
β¨ π₯ = π΄) β ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄))) |
112 | 108, 111 | orbi12d 918 |
. . . . . . . . . . 11
β’ (π₯ = (π΄ β {π¦}) β ((Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β
β¨ π₯ = π΄)) β (Β¬ (π΄ β (π΄ β {π¦})) β Fin β¨ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄)))) |
113 | 112, 27 | elrab2 3653 |
. . . . . . . . . 10
β’ ((π΄ β {π¦}) β π β ((π΄ β {π¦}) β π« π΄ β§ (Β¬ (π΄ β (π΄ β {π¦})) β Fin β¨ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄)))) |
114 | 85 | biantrurd 534 |
. . . . . . . . . 10
β’ (π β (TopOnβπ΄) β ((Β¬ (π΄ β (π΄ β {π¦})) β Fin β¨ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄)) β ((π΄ β {π¦}) β π« π΄ β§ (Β¬ (π΄ β (π΄ β {π¦})) β Fin β¨ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄))))) |
115 | 113, 114 | bitr4id 290 |
. . . . . . . . 9
β’ (π β (TopOnβπ΄) β ((π΄ β {π¦}) β π β (Β¬ (π΄ β (π΄ β {π¦})) β Fin β¨ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄)))) |
116 | | dfin4 4232 |
. . . . . . . . . . 11
β’ (π΄ β© {π¦}) = (π΄ β (π΄ β {π¦})) |
117 | | inss2 4194 |
. . . . . . . . . . . 12
β’ (π΄ β© {π¦}) β {π¦} |
118 | | ssfi 9124 |
. . . . . . . . . . . 12
β’ (({π¦} β Fin β§ (π΄ β© {π¦}) β {π¦}) β (π΄ β© {π¦}) β Fin) |
119 | 17, 117, 118 | mp2an 691 |
. . . . . . . . . . 11
β’ (π΄ β© {π¦}) β Fin |
120 | 116, 119 | eqeltrri 2835 |
. . . . . . . . . 10
β’ (π΄ β (π΄ β {π¦})) β Fin |
121 | | biortn 937 |
. . . . . . . . . 10
β’ ((π΄ β (π΄ β {π¦})) β Fin β (((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄) β (Β¬ (π΄ β (π΄ β {π¦})) β Fin β¨ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄)))) |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . 9
β’ (((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄) β (Β¬ (π΄ β (π΄ β {π¦})) β Fin β¨ ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄))) |
123 | 115, 122 | bitr4di 289 |
. . . . . . . 8
β’ (π β (TopOnβπ΄) β ((π΄ β {π¦}) β π β ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄))) |
124 | 123 | ad2antll 728 |
. . . . . . 7
β’ ((π¦ β π΄ β§ (Β¬ π΄ β Fin β§ π β (TopOnβπ΄))) β ((π΄ β {π¦}) β π β ((π΄ β {π¦}) = β
β¨ (π΄ β {π¦}) = π΄))) |
125 | 105, 124 | mtbird 325 |
. . . . . 6
β’ ((π¦ β π΄ β§ (Β¬ π΄ β Fin β§ π β (TopOnβπ΄))) β Β¬ (π΄ β {π¦}) β π) |
126 | 125 | expcom 415 |
. . . . 5
β’ ((Β¬
π΄ β Fin β§ π β (TopOnβπ΄)) β (π¦ β π΄ β Β¬ (π΄ β {π¦}) β π)) |
127 | | nelneq2 2863 |
. . . . . 6
β’ (((π΄ β {π¦}) β π« π΄ β§ Β¬ (π΄ β {π¦}) β π) β Β¬ π« π΄ = π) |
128 | | eqcom 2744 |
. . . . . 6
β’ (π = π« π΄ β π« π΄ = π) |
129 | 127, 128 | sylnibr 329 |
. . . . 5
β’ (((π΄ β {π¦}) β π« π΄ β§ Β¬ (π΄ β {π¦}) β π) β Β¬ π = π« π΄) |
130 | 86, 126, 129 | syl6an 683 |
. . . 4
β’ ((Β¬
π΄ β Fin β§ π β (TopOnβπ΄)) β (π¦ β π΄ β Β¬ π = π« π΄)) |
131 | 79, 130 | exellimddv 35845 |
. . 3
β’ ((Β¬
π΄ β Fin β§ π β (TopOnβπ΄)) β Β¬ π = π« π΄) |
132 | 77, 131 | pm2.65da 816 |
. 2
β’ (Β¬
π΄ β Fin β Β¬
π β (TopOnβπ΄)) |
133 | 132 | con4i 114 |
1
β’ (π β (TopOnβπ΄) β π΄ β Fin) |