Metamath Proof Explorer

Theorem isacs

Description: A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isacs ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝑋 ∈ V )
2 elfvex ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ V )
3 2 adantr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) → 𝑋 ∈ V )
4 fveq2 ⊢ ( 𝑥 = 𝑋 → ( Moore ‘ 𝑥 ) = ( Moore ‘ 𝑋 ) )
5 pweq ⊢ ( 𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋 )
6 5 5 feq23d ⊢ ( 𝑥 = 𝑋 → ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ↔ 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) )
7 5 raleqdv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) )
8 6 7 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ↔ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )
9 8 exbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )
10 4 9 rabeqbidv ⊢ ( 𝑥 = 𝑋 → { 𝑐 ∈ ( Moore ‘ 𝑥 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } = { 𝑐 ∈ ( Moore ‘ 𝑋 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } )
11 df-acs ⊢ ACS = ( 𝑥 ∈ V ↦ { 𝑐 ∈ ( Moore ‘ 𝑥 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } )
12 fvex ⊢ ( Moore ‘ 𝑋 ) ∈ V
13 12 rabex ⊢ { 𝑐 ∈ ( Moore ‘ 𝑋 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } ∈ V
14 10 11 13 fvmpt ⊢ ( 𝑋 ∈ V → ( ACS ‘ 𝑋 ) = { 𝑐 ∈ ( Moore ‘ 𝑋 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } )
15 14 eleq2d ⊢ ( 𝑋 ∈ V → ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ 𝐶 ∈ { 𝑐 ∈ ( Moore ‘ 𝑋 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } ) )
16 eleq2 ⊢ ( 𝑐 = 𝐶 → ( 𝑠 ∈ 𝑐 ↔ 𝑠 ∈ 𝐶 ) )
17 16 bibi1d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ↔ ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) )
18 17 ralbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) )
19 18 anbi2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ↔ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )
20 19 exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )
21 20 elrab ⊢ ( 𝐶 ∈ { 𝑐 ∈ ( Moore ‘ 𝑋 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )
22 15 21 syl6bb ⊢ ( 𝑋 ∈ V → ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) ) )
23 1 3 22 pm5.21nii ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )