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 ) ) )