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 ∈ 𝒫 X F ⁡ s = ⋃ F 𝒫 s ∩ Fin

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢ F = mrCls ⁡ C
2 isacs3lem ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
3 1 isacs4lem ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
4 1 isacs5lem ⊢ C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t → C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X F ⁡ s = ⋃ F 𝒫 s ∩ Fin
5 2 3 4 3syl ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X F ⁡ s = ⋃ F 𝒫 s ∩ Fin
6 simpl ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X F ⁡ 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 ∩ Fin F ⁡ t = ⋃ F 𝒫 s ∩ Fin
15 12 13 14 3syl ⊢ C ∈ Moore ⁡ X → ⋃ t ∈ 𝒫 s ∩ Fin F ⁡ t = ⋃ F 𝒫 s ∩ Fin
16 15 ad2antrr ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 X ∧ F ⁡ s = ⋃ F 𝒫 s ∩ Fin → ⋃ t ∈ 𝒫 s ∩ Fin F ⁡ t = ⋃ F 𝒫 s ∩ Fin
17 11 16 eqtr4d ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 X ∧ F ⁡ s = ⋃ F 𝒫 s ∩ Fin → F ⁡ s = ⋃ t ∈ 𝒫 s ∩ Fin F ⁡ t
18 17 sseq1d ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 X ∧ F ⁡ s = ⋃ F 𝒫 s ∩ Fin → F ⁡ s ⊆ s ↔ ⋃ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
19 iunss ⊢ ⋃ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s ↔ ∀ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
20 18 19 bitrdi ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 X ∧ F ⁡ s = ⋃ F 𝒫 s ∩ Fin → F ⁡ s ⊆ s ↔ ∀ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
21 10 20 bitrd ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 X ∧ F ⁡ s = ⋃ F 𝒫 s ∩ Fin → s ∈ C ↔ ∀ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
22 21 ex ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 X → F ⁡ s = ⋃ F 𝒫 s ∩ Fin → s ∈ C ↔ ∀ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
23 22 ralimdva ⊢ C ∈ Moore ⁡ X → ∀ s ∈ 𝒫 X F ⁡ s = ⋃ F 𝒫 s ∩ Fin → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
24 23 imp ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X F ⁡ s = ⋃ F 𝒫 s ∩ Fin → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
25 1 isacs2 ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ t ∈ 𝒫 s ∩ Fin F ⁡ t ⊆ s
26 6 24 25 sylanbrc ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X F ⁡ s = ⋃ F 𝒫 s ∩ Fin → C ∈ ACS ⁡ X
27 5 26 impbii ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X F ⁡ s = ⋃ F 𝒫 s ∩ Fin