This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acsfiel

Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis isacs2.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion acsfiel ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isacs2.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 acsmre ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
3 mress ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ⊆ 𝑋 )
4 2 3 sylan ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ⊆ 𝑋 )
5 4 ex ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 → 𝑆 ⊆ 𝑋 ) )
6 5 pm4.71rd ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ∈ 𝐶 ) ) )
7 eleq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ 𝐶 ↔ 𝑆 ∈ 𝐶 ) )
8 pweq ⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
9 8 ineq1d ⊢ ( 𝑠 = 𝑆 → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 𝑆 ∩ Fin ) )
10 sseq2 ⊢ ( 𝑠 = 𝑆 → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ↔ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )
11 9 10 raleqbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )
12 7 11 bibi12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ↔ ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )
13 1 isacs2 ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
14 13 simprbi ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
15 14 adantr ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
16 elfvdm ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝑋 ∈ dom ACS )
17 elpw2g ⊢ ( 𝑋 ∈ dom ACS → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
18 16 17 syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
19 18 biimpar ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
20 12 15 19 rspcdva ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )
21 20 pm5.32da ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ∈ 𝐶 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )
22 6 21 bitrd ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )