This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A set is closed in an algebraic closure system iff it contains all
closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015)
|
|
Ref |
Expression |
|
Hypothesis |
isacs2.f |
⊢ 𝐹 = ( mrCls ‘ 𝐶 ) |
|
Assertion |
acsfiel2 |
⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isacs2.f |
⊢ 𝐹 = ( mrCls ‘ 𝐶 ) |
| 2 |
1
|
acsfiel |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) ) |
| 3 |
2
|
baibd |
⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) |