Metamath Proof Explorer

Theorem isacs5

Description: A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f ⊢F=mrCls⁡C
Assertion isacs5 ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢F=mrCls⁡C
2 isacs3lem ⊢C∈ACS⁡X→C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈C
3 1 isacs4lem ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈C→C∈Moore⁡X∧∀t∈𝒫𝒫XtoInc⁡t∈Dirset→F⁡⋃t=⋃Ft
4 1 isacs5lem ⊢C∈Moore⁡X∧∀t∈𝒫𝒫XtoInc⁡t∈Dirset→F⁡⋃t=⋃Ft→C∈Moore⁡X∧∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin
5 2 3 4 3syl ⊢C∈ACS⁡X→C∈Moore⁡X∧∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin
6 simpl ⊢C∈Moore⁡X∧∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin→C∈Moore⁡X
7 elpwi ⊢s∈𝒫X→s⊆X
8 1 mrcidb2 ⊢C∈Moore⁡X∧s⊆X→s∈C↔F⁡s⊆s
9 7 8 sylan2 ⊢C∈Moore⁡X∧s∈𝒫X→s∈C↔F⁡s⊆s
10 9 adantr ⊢C∈Moore⁡X∧s∈𝒫X∧F⁡s=⋃F𝒫s∩Fin→s∈C↔F⁡s⊆s
11 simpr ⊢C∈Moore⁡X∧s∈𝒫X∧F⁡s=⋃F𝒫s∩Fin→F⁡s=⋃F𝒫s∩Fin
12 1 mrcf ⊢C∈Moore⁡X→F:𝒫X⟶C
13 ffun ⊢F:𝒫X⟶C→Fun⁡F
14 funiunfv ⊢Fun⁡F→⋃t∈𝒫s∩FinF⁡t=⋃F𝒫s∩Fin
15 12 13 14 3syl ⊢C∈Moore⁡X→⋃t∈𝒫s∩FinF⁡t=⋃F𝒫s∩Fin
16 15 ad2antrr ⊢C∈Moore⁡X∧s∈𝒫X∧F⁡s=⋃F𝒫s∩Fin→⋃t∈𝒫s∩FinF⁡t=⋃F𝒫s∩Fin
17 11 16 eqtr4d ⊢C∈Moore⁡X∧s∈𝒫X∧F⁡s=⋃F𝒫s∩Fin→F⁡s=⋃t∈𝒫s∩FinF⁡t
18 17 sseq1d ⊢C∈Moore⁡X∧s∈𝒫X∧F⁡s=⋃F𝒫s∩Fin→F⁡s⊆s↔⋃t∈𝒫s∩FinF⁡t⊆s
19 iunss ⊢⋃t∈𝒫s∩FinF⁡t⊆s↔∀t∈𝒫s∩FinF⁡t⊆s
20 18 19 bitrdi ⊢C∈Moore⁡X∧s∈𝒫X∧F⁡s=⋃F𝒫s∩Fin→F⁡s⊆s↔∀t∈𝒫s∩FinF⁡t⊆s
21 10 20 bitrd ⊢C∈Moore⁡X∧s∈𝒫X∧F⁡s=⋃F𝒫s∩Fin→s∈C↔∀t∈𝒫s∩FinF⁡t⊆s
22 21 ex ⊢C∈Moore⁡X∧s∈𝒫X→F⁡s=⋃F𝒫s∩Fin→s∈C↔∀t∈𝒫s∩FinF⁡t⊆s
23 22 ralimdva ⊢C∈Moore⁡X→∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin→∀s∈𝒫Xs∈C↔∀t∈𝒫s∩FinF⁡t⊆s
24 23 imp ⊢C∈Moore⁡X∧∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin→∀s∈𝒫Xs∈C↔∀t∈𝒫s∩FinF⁡t⊆s
25 1 isacs2 ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀s∈𝒫Xs∈C↔∀t∈𝒫s∩FinF⁡t⊆s
26 6 24 25 sylanbrc ⊢C∈Moore⁡X∧∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin→C∈ACS⁡X
27 5 26 impbii ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀s∈𝒫XF⁡s=⋃F𝒫s∩Fin