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

Metamath Proof Explorer

Theorem acsficl

Description: A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion acsficl ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑆 ) = ∪ ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 fveq2 ⊢ ( 𝑠 = 𝑆 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑆 ) )
3 pweq ⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
4 3 ineq1d ⊢ ( 𝑠 = 𝑆 → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 𝑆 ∩ Fin ) )
5 4 imaeq2d ⊢ ( 𝑠 = 𝑆 → ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) )
6 5 unieqd ⊢ ( 𝑠 = 𝑆 → ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ∪ ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) )
7 2 6 eqeq12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ↔ ( 𝐹 ‘ 𝑆 ) = ∪ ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) ) )
8 isacs3lem ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) )
9 1 isacs4lem ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) )
10 1 isacs5lem ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )
11 8 9 10 3syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )
12 11 simprd ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
13 12 adantr ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
14 elfvdm ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝑋 ∈ dom ACS )
15 elpw2g ⊢ ( 𝑋 ∈ dom ACS → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
16 14 15 syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
17 16 biimpar ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
18 7 13 17 rspcdva ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑆 ) = ∪ ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) )