Step | Hyp | Ref
| Expression |
1 | | elpwi 4609 |
. . . . 5
β’ (π₯ β π« π β π₯ β π) |
2 | | ufilb 23417 |
. . . . . . . . . 10
β’ ((πΉ β (UFilβπ) β§ π₯ β π) β (Β¬ π₯ β πΉ β (π β π₯) β πΉ)) |
3 | 2 | adantr 481 |
. . . . . . . . 9
β’ (((πΉ β (UFilβπ) β§ π₯ β π) β§ (π β π₯) β Fin) β (Β¬ π₯ β πΉ β (π β π₯) β πΉ)) |
4 | | ufilfil 23415 |
. . . . . . . . . . . 12
β’ (πΉ β (UFilβπ) β πΉ β (Filβπ)) |
5 | 4 | adantr 481 |
. . . . . . . . . . 11
β’ ((πΉ β (UFilβπ) β§ π₯ β π) β πΉ β (Filβπ)) |
6 | | filfinnfr 23388 |
. . . . . . . . . . . . 13
β’ ((πΉ β (Filβπ) β§ (π β π₯) β πΉ β§ (π β π₯) β Fin) β β© πΉ
β β
) |
7 | 6 | 3exp 1119 |
. . . . . . . . . . . 12
β’ (πΉ β (Filβπ) β ((π β π₯) β πΉ β ((π β π₯) β Fin β β© πΉ
β β
))) |
8 | 7 | com23 86 |
. . . . . . . . . . 11
β’ (πΉ β (Filβπ) β ((π β π₯) β Fin β ((π β π₯) β πΉ β β© πΉ β
β
))) |
9 | 5, 8 | syl 17 |
. . . . . . . . . 10
β’ ((πΉ β (UFilβπ) β§ π₯ β π) β ((π β π₯) β Fin β ((π β π₯) β πΉ β β© πΉ β
β
))) |
10 | 9 | imp 407 |
. . . . . . . . 9
β’ (((πΉ β (UFilβπ) β§ π₯ β π) β§ (π β π₯) β Fin) β ((π β π₯) β πΉ β β© πΉ β β
)) |
11 | 3, 10 | sylbid 239 |
. . . . . . . 8
β’ (((πΉ β (UFilβπ) β§ π₯ β π) β§ (π β π₯) β Fin) β (Β¬ π₯ β πΉ β β© πΉ β β
)) |
12 | 11 | necon4bd 2960 |
. . . . . . 7
β’ (((πΉ β (UFilβπ) β§ π₯ β π) β§ (π β π₯) β Fin) β (β© πΉ =
β
β π₯ β
πΉ)) |
13 | 12 | ex 413 |
. . . . . 6
β’ ((πΉ β (UFilβπ) β§ π₯ β π) β ((π β π₯) β Fin β (β© πΉ =
β
β π₯ β
πΉ))) |
14 | 13 | com23 86 |
. . . . 5
β’ ((πΉ β (UFilβπ) β§ π₯ β π) β (β© πΉ = β
β ((π β π₯) β Fin β π₯ β πΉ))) |
15 | 1, 14 | sylan2 593 |
. . . 4
β’ ((πΉ β (UFilβπ) β§ π₯ β π« π) β (β© πΉ = β
β ((π β π₯) β Fin β π₯ β πΉ))) |
16 | 15 | ralrimdva 3154 |
. . 3
β’ (πΉ β (UFilβπ) β (β© πΉ =
β
β βπ₯
β π« π((π β π₯) β Fin β π₯ β πΉ))) |
17 | 4 | adantr 481 |
. . . . . . . . . . . 12
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β πΉ β (Filβπ)) |
18 | | uffixsn 23436 |
. . . . . . . . . . . 12
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β {π¦} β πΉ) |
19 | | filelss 23363 |
. . . . . . . . . . . 12
β’ ((πΉ β (Filβπ) β§ {π¦} β πΉ) β {π¦} β π) |
20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β {π¦} β π) |
21 | | dfss4 4258 |
. . . . . . . . . . 11
β’ ({π¦} β π β (π β (π β {π¦})) = {π¦}) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . 10
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (π β (π β {π¦})) = {π¦}) |
23 | | snfi 9046 |
. . . . . . . . . 10
β’ {π¦} β Fin |
24 | 22, 23 | eqeltrdi 2841 |
. . . . . . . . 9
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (π β (π β {π¦})) β Fin) |
25 | | difss 4131 |
. . . . . . . . . . 11
β’ (π β {π¦}) β π |
26 | | filtop 23366 |
. . . . . . . . . . . 12
β’ (πΉ β (Filβπ) β π β πΉ) |
27 | | elpw2g 5344 |
. . . . . . . . . . . 12
β’ (π β πΉ β ((π β {π¦}) β π« π β (π β {π¦}) β π)) |
28 | 17, 26, 27 | 3syl 18 |
. . . . . . . . . . 11
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β ((π β {π¦}) β π« π β (π β {π¦}) β π)) |
29 | 25, 28 | mpbiri 257 |
. . . . . . . . . 10
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (π β {π¦}) β π« π) |
30 | | difeq2 4116 |
. . . . . . . . . . . . 13
β’ (π₯ = (π β {π¦}) β (π β π₯) = (π β (π β {π¦}))) |
31 | 30 | eleq1d 2818 |
. . . . . . . . . . . 12
β’ (π₯ = (π β {π¦}) β ((π β π₯) β Fin β (π β (π β {π¦})) β Fin)) |
32 | | eleq1 2821 |
. . . . . . . . . . . 12
β’ (π₯ = (π β {π¦}) β (π₯ β πΉ β (π β {π¦}) β πΉ)) |
33 | 31, 32 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π₯ = (π β {π¦}) β (((π β π₯) β Fin β π₯ β πΉ) β ((π β (π β {π¦})) β Fin β (π β {π¦}) β πΉ))) |
34 | 33 | rspcv 3608 |
. . . . . . . . . 10
β’ ((π β {π¦}) β π« π β (βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ) β ((π β (π β {π¦})) β Fin β (π β {π¦}) β πΉ))) |
35 | 29, 34 | syl 17 |
. . . . . . . . 9
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ) β ((π β (π β {π¦})) β Fin β (π β {π¦}) β πΉ))) |
36 | 24, 35 | mpid 44 |
. . . . . . . 8
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ) β (π β {π¦}) β πΉ)) |
37 | | ufilb 23417 |
. . . . . . . . . 10
β’ ((πΉ β (UFilβπ) β§ {π¦} β π) β (Β¬ {π¦} β πΉ β (π β {π¦}) β πΉ)) |
38 | 20, 37 | syldan 591 |
. . . . . . . . 9
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (Β¬ {π¦} β πΉ β (π β {π¦}) β πΉ)) |
39 | 18 | pm2.24d 151 |
. . . . . . . . 9
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (Β¬ {π¦} β πΉ β Β¬ π¦ β β© πΉ)) |
40 | 38, 39 | sylbird 259 |
. . . . . . . 8
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β ((π β {π¦}) β πΉ β Β¬ π¦ β β© πΉ)) |
41 | 36, 40 | syld 47 |
. . . . . . 7
β’ ((πΉ β (UFilβπ) β§ π¦ β β© πΉ) β (βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ) β Β¬ π¦ β β© πΉ)) |
42 | 41 | impancom 452 |
. . . . . 6
β’ ((πΉ β (UFilβπ) β§ βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ)) β (π¦ β β© πΉ β Β¬ π¦ β β© πΉ)) |
43 | 42 | pm2.01d 189 |
. . . . 5
β’ ((πΉ β (UFilβπ) β§ βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ)) β Β¬ π¦ β β© πΉ) |
44 | 43 | eq0rdv 4404 |
. . . 4
β’ ((πΉ β (UFilβπ) β§ βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ)) β β© πΉ = β
) |
45 | 44 | ex 413 |
. . 3
β’ (πΉ β (UFilβπ) β (βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ) β β© πΉ = β
)) |
46 | 16, 45 | impbid 211 |
. 2
β’ (πΉ β (UFilβπ) β (β© πΉ =
β
β βπ₯
β π« π((π β π₯) β Fin β π₯ β πΉ))) |
47 | | rabss 4069 |
. 2
β’ ({π₯ β π« π β£ (π β π₯) β Fin} β πΉ β βπ₯ β π« π((π β π₯) β Fin β π₯ β πΉ)) |
48 | 46, 47 | bitr4di 288 |
1
β’ (πΉ β (UFilβπ) β (β© πΉ =
β
β {π₯ β
π« π β£ (π β π₯) β Fin} β πΉ)) |