Step | Hyp | Ref
| Expression |
1 | | locfincmp.1 |
. . . . . . . . . 10
β’ π = βͺ
π½ |
2 | 1 | locfinnei 22897 |
. . . . . . . . 9
β’ ((πΆ β (LocFinβπ½) β§ π₯ β π) β βπ β π½ (π₯ β π β§ {π β πΆ β£ (π β© π) β β
} β Fin)) |
3 | 2 | ralrimiva 3140 |
. . . . . . . 8
β’ (πΆ β (LocFinβπ½) β βπ₯ β π βπ β π½ (π₯ β π β§ {π β πΆ β£ (π β© π) β β
} β Fin)) |
4 | 1 | cmpcov2 22764 |
. . . . . . . 8
β’ ((π½ β Comp β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β πΆ β£ (π β© π) β β
} β Fin)) β
βπ β (π«
π½ β© Fin)(π = βͺ
π β§ βπ β π {π β πΆ β£ (π β© π) β β
} β Fin)) |
5 | 3, 4 | sylan2 594 |
. . . . . . 7
β’ ((π½ β Comp β§ πΆ β (LocFinβπ½)) β βπ β (π« π½ β© Fin)(π = βͺ π β§ βπ β π {π β πΆ β£ (π β© π) β β
} β Fin)) |
6 | | elfpw 9304 |
. . . . . . . . 9
β’ (π β (π« π½ β© Fin) β (π β π½ β§ π β Fin)) |
7 | | simplrr 777 |
. . . . . . . . . . 11
β’ ((((π½ β Comp β§ πΆ β (LocFinβπ½)) β§ (π β π½ β§ π β Fin)) β§ π = βͺ π) β π β Fin) |
8 | | eldifsn 4751 |
. . . . . . . . . . . . 13
β’ (π₯ β (πΆ β {β
}) β (π₯ β πΆ β§ π₯ β β
)) |
9 | | ineq1 4169 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β (π β© π) = (π₯ β© π)) |
10 | 9 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π₯ β ((π β© π) β β
β (π₯ β© π) β β
)) |
11 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β§ (π β π β§ π¦ β π)) β π₯ β πΆ) |
12 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β§ (π β π β§ π¦ β π)) β π¦ β π₯) |
13 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β§ (π β π β§ π¦ β π)) β π¦ β π) |
14 | | inelcm 4428 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β π₯ β§ π¦ β π) β (π₯ β© π) β β
) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β§ (π β π β§ π¦ β π)) β (π₯ β© π) β β
) |
16 | 10, 11, 15 | elrabd 3651 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β§ (π β π β§ π¦ β π)) β π₯ β {π β πΆ β£ (π β© π) β β
}) |
17 | | elunii 4874 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β π₯ β§ π₯ β πΆ) β π¦ β βͺ πΆ) |
18 | | locfincmp.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ π = βͺ
πΆ |
19 | 17, 18 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β π₯ β§ π₯ β πΆ) β π¦ β π) |
20 | 19 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β πΆ β§ π¦ β π₯) β π¦ β π) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β π¦ β π) |
22 | 1, 18 | locfinbas 22896 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΆ β (LocFinβπ½) β π = π) |
23 | 22 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π½ β Comp β§ πΆ β (LocFinβπ½)) β π = π) |
24 | 23 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β π = π) |
25 | 21, 24 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β π¦ β π) |
26 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β π = βͺ π) |
27 | 25, 26 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β π¦ β βͺ π) |
28 | | eluni2 4873 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β βͺ π
β βπ β
π π¦ β π) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β βπ β π π¦ β π) |
30 | 16, 29 | reximddv 3165 |
. . . . . . . . . . . . . . . . 17
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ (π₯ β πΆ β§ π¦ β π₯)) β βπ β π π₯ β {π β πΆ β£ (π β© π) β β
}) |
31 | 30 | expr 458 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ π₯ β πΆ) β (π¦ β π₯ β βπ β π π₯ β {π β πΆ β£ (π β© π) β β
})) |
32 | 31 | exlimdv 1937 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ π₯ β πΆ) β (βπ¦ π¦ β π₯ β βπ β π π₯ β {π β πΆ β£ (π β© π) β β
})) |
33 | | n0 4310 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β
β
βπ¦ π¦ β π₯) |
34 | | eliun 4962 |
. . . . . . . . . . . . . . 15
β’ (π₯ β βͺ π β π {π β πΆ β£ (π β© π) β β
} β βπ β π π₯ β {π β πΆ β£ (π β© π) β β
}) |
35 | 32, 33, 34 | 3imtr4g 296 |
. . . . . . . . . . . . . 14
β’
(((((π½ β Comp
β§ πΆ β
(LocFinβπ½)) β§
(π β π½ β§ π β Fin)) β§ π = βͺ π) β§ π₯ β πΆ) β (π₯ β β
β π₯ β βͺ
π β π {π β πΆ β£ (π β© π) β β
})) |
36 | 35 | expimpd 455 |
. . . . . . . . . . . . 13
β’ ((((π½ β Comp β§ πΆ β (LocFinβπ½)) β§ (π β π½ β§ π β Fin)) β§ π = βͺ π) β ((π₯ β πΆ β§ π₯ β β
) β π₯ β βͺ
π β π {π β πΆ β£ (π β© π) β β
})) |
37 | 8, 36 | biimtrid 241 |
. . . . . . . . . . . 12
β’ ((((π½ β Comp β§ πΆ β (LocFinβπ½)) β§ (π β π½ β§ π β Fin)) β§ π = βͺ π) β (π₯ β (πΆ β {β
}) β π₯ β βͺ π β π {π β πΆ β£ (π β© π) β β
})) |
38 | 37 | ssrdv 3954 |
. . . . . . . . . . 11
β’ ((((π½ β Comp β§ πΆ β (LocFinβπ½)) β§ (π β π½ β§ π β Fin)) β§ π = βͺ π) β (πΆ β {β
}) β βͺ π β π {π β πΆ β£ (π β© π) β β
}) |
39 | | iunfi 9290 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ βπ β π {π β πΆ β£ (π β© π) β β
} β Fin) β βͺ π β π {π β πΆ β£ (π β© π) β β
} β Fin) |
40 | 39 | ex 414 |
. . . . . . . . . . . 12
β’ (π β Fin β
(βπ β π {π β πΆ β£ (π β© π) β β
} β Fin β βͺ π β π {π β πΆ β£ (π β© π) β β
} β Fin)) |
41 | | ssfi 9123 |
. . . . . . . . . . . . 13
β’
((βͺ π β π {π β πΆ β£ (π β© π) β β
} β Fin β§ (πΆ β {β
}) β
βͺ π β π {π β πΆ β£ (π β© π) β β
}) β (πΆ β {β
}) β
Fin) |
42 | 41 | expcom 415 |
. . . . . . . . . . . 12
β’ ((πΆ β {β
}) β
βͺ π β π {π β πΆ β£ (π β© π) β β
} β (βͺ π β π {π β πΆ β£ (π β© π) β β
} β Fin β (πΆ β {β
}) β
Fin)) |
43 | 40, 42 | sylan9 509 |
. . . . . . . . . . 11
β’ ((π β Fin β§ (πΆ β {β
}) β
βͺ π β π {π β πΆ β£ (π β© π) β β
}) β (βπ β π {π β πΆ β£ (π β© π) β β
} β Fin β (πΆ β {β
}) β
Fin)) |
44 | 7, 38, 43 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π½ β Comp β§ πΆ β (LocFinβπ½)) β§ (π β π½ β§ π β Fin)) β§ π = βͺ π) β (βπ β π {π β πΆ β£ (π β© π) β β
} β Fin β (πΆ β {β
}) β
Fin)) |
45 | 44 | expimpd 455 |
. . . . . . . . 9
β’ (((π½ β Comp β§ πΆ β (LocFinβπ½)) β§ (π β π½ β§ π β Fin)) β ((π = βͺ π β§ βπ β π {π β πΆ β£ (π β© π) β β
} β Fin) β (πΆ β {β
}) β
Fin)) |
46 | 6, 45 | sylan2b 595 |
. . . . . . . 8
β’ (((π½ β Comp β§ πΆ β (LocFinβπ½)) β§ π β (π« π½ β© Fin)) β ((π = βͺ π β§ βπ β π {π β πΆ β£ (π β© π) β β
} β Fin) β (πΆ β {β
}) β
Fin)) |
47 | 46 | rexlimdva 3149 |
. . . . . . 7
β’ ((π½ β Comp β§ πΆ β (LocFinβπ½)) β (βπ β (π« π½ β© Fin)(π = βͺ π β§ βπ β π {π β πΆ β£ (π β© π) β β
} β Fin) β (πΆ β {β
}) β
Fin)) |
48 | 5, 47 | mpd 15 |
. . . . . 6
β’ ((π½ β Comp β§ πΆ β (LocFinβπ½)) β (πΆ β {β
}) β
Fin) |
49 | | snfi 8994 |
. . . . . 6
β’ {β
}
β Fin |
50 | | unfi 9122 |
. . . . . 6
β’ (((πΆ β {β
}) β Fin
β§ {β
} β Fin) β ((πΆ β {β
}) βͺ {β
}) β
Fin) |
51 | 48, 49, 50 | sylancl 587 |
. . . . 5
β’ ((π½ β Comp β§ πΆ β (LocFinβπ½)) β ((πΆ β {β
}) βͺ {β
}) β
Fin) |
52 | | ssun1 4136 |
. . . . . 6
β’ πΆ β (πΆ βͺ {β
}) |
53 | | undif1 4439 |
. . . . . 6
β’ ((πΆ β {β
}) βͺ
{β
}) = (πΆ βͺ
{β
}) |
54 | 52, 53 | sseqtrri 3985 |
. . . . 5
β’ πΆ β ((πΆ β {β
}) βͺ
{β
}) |
55 | | ssfi 9123 |
. . . . 5
β’ ((((πΆ β {β
}) βͺ
{β
}) β Fin β§ πΆ β ((πΆ β {β
}) βͺ {β
})) β
πΆ β
Fin) |
56 | 51, 54, 55 | sylancl 587 |
. . . 4
β’ ((π½ β Comp β§ πΆ β (LocFinβπ½)) β πΆ β Fin) |
57 | 56, 23 | jca 513 |
. . 3
β’ ((π½ β Comp β§ πΆ β (LocFinβπ½)) β (πΆ β Fin β§ π = π)) |
58 | 57 | ex 414 |
. 2
β’ (π½ β Comp β (πΆ β (LocFinβπ½) β (πΆ β Fin β§ π = π))) |
59 | | cmptop 22769 |
. . 3
β’ (π½ β Comp β π½ β Top) |
60 | 1, 18 | finlocfin 22894 |
. . . 4
β’ ((π½ β Top β§ πΆ β Fin β§ π = π) β πΆ β (LocFinβπ½)) |
61 | 60 | 3expib 1123 |
. . 3
β’ (π½ β Top β ((πΆ β Fin β§ π = π) β πΆ β (LocFinβπ½))) |
62 | 59, 61 | syl 17 |
. 2
β’ (π½ β Comp β ((πΆ β Fin β§ π = π) β πΆ β (LocFinβπ½))) |
63 | 58, 62 | impbid 211 |
1
β’ (π½ β Comp β (πΆ β (LocFinβπ½) β (πΆ β Fin β§ π = π))) |