Metamath Proof Explorer


Theorem isacs5lem

Description: If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f F = mrCls C
Assertion isacs5lem C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t C Moore X s 𝒫 X F s = F 𝒫 s Fin

Proof

Step Hyp Ref Expression
1 acsdrscl.f F = mrCls C
2 unifpw 𝒫 s Fin = s
3 2 fveq2i F 𝒫 s Fin = F s
4 vex s V
5 fpwipodrs s V toInc 𝒫 s Fin Dirset
6 4 5 mp1i C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X toInc 𝒫 s Fin Dirset
7 fveq2 t = 𝒫 s Fin toInc t = toInc 𝒫 s Fin
8 7 eleq1d t = 𝒫 s Fin toInc t Dirset toInc 𝒫 s Fin Dirset
9 unieq t = 𝒫 s Fin t = 𝒫 s Fin
10 9 fveq2d t = 𝒫 s Fin F t = F 𝒫 s Fin
11 imaeq2 t = 𝒫 s Fin F t = F 𝒫 s Fin
12 11 unieqd t = 𝒫 s Fin F t = F 𝒫 s Fin
13 10 12 eqeq12d t = 𝒫 s Fin F t = F t F 𝒫 s Fin = F 𝒫 s Fin
14 8 13 imbi12d t = 𝒫 s Fin toInc t Dirset F t = F t toInc 𝒫 s Fin Dirset F 𝒫 s Fin = F 𝒫 s Fin
15 simplr C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X t 𝒫 𝒫 X toInc t Dirset F t = F t
16 inss1 𝒫 s Fin 𝒫 s
17 elpwi s 𝒫 X s X
18 17 sspwd s 𝒫 X 𝒫 s 𝒫 X
19 18 adantl C Moore X s 𝒫 X 𝒫 s 𝒫 X
20 16 19 sstrid C Moore X s 𝒫 X 𝒫 s Fin 𝒫 X
21 vpwex 𝒫 s V
22 21 inex1 𝒫 s Fin V
23 22 elpw 𝒫 s Fin 𝒫 𝒫 X 𝒫 s Fin 𝒫 X
24 20 23 sylibr C Moore X s 𝒫 X 𝒫 s Fin 𝒫 𝒫 X
25 24 adantlr C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X 𝒫 s Fin 𝒫 𝒫 X
26 14 15 25 rspcdva C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X toInc 𝒫 s Fin Dirset F 𝒫 s Fin = F 𝒫 s Fin
27 6 26 mpd C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X F 𝒫 s Fin = F 𝒫 s Fin
28 3 27 eqtr3id C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X F s = F 𝒫 s Fin
29 28 ralrimiva C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X F s = F 𝒫 s Fin
30 29 ex C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t s 𝒫 X F s = F 𝒫 s Fin
31 30 imdistani C Moore X t 𝒫 𝒫 X toInc t Dirset F t = F t C Moore X s 𝒫 X F s = F 𝒫 s Fin