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 ⊢C∈ACS⁡X↔C∈Moore⁡X∧∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s

Proof

Step Hyp Ref Expression
1 elfvex ⊢C∈ACS⁡X→X∈V
2 elfvex ⊢C∈Moore⁡X→X∈V
3 2 adantr ⊢C∈Moore⁡X∧∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s→X∈V
4 fveq2 ⊢x=X→Moore⁡x=Moore⁡X
5 pweq ⊢x=X→𝒫x=𝒫X
6 5 5 feq23d ⊢x=X→f:𝒫x⟶𝒫x↔f:𝒫X⟶𝒫X
7 5 raleqdv ⊢x=X→∀s∈𝒫xs∈c↔⋃f𝒫s∩Fin⊆s↔∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s
8 6 7 anbi12d ⊢x=X→f:𝒫x⟶𝒫x∧∀s∈𝒫xs∈c↔⋃f𝒫s∩Fin⊆s↔f:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s
9 8 exbidv ⊢x=X→∃ff:𝒫x⟶𝒫x∧∀s∈𝒫xs∈c↔⋃f𝒫s∩Fin⊆s↔∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s
10 4 9 rabeqbidv ⊢x=X→c∈Moore⁡x|∃ff:𝒫x⟶𝒫x∧∀s∈𝒫xs∈c↔⋃f𝒫s∩Fin⊆s=c∈Moore⁡X|∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s
11 df-acs ⊢ACS=x∈V⟼c∈Moore⁡x|∃ff:𝒫x⟶𝒫x∧∀s∈𝒫xs∈c↔⋃f𝒫s∩Fin⊆s
12 fvex ⊢Moore⁡X∈V
13 12 rabex ⊢c∈Moore⁡X|∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s∈V
14 10 11 13 fvmpt ⊢X∈V→ACS⁡X=c∈Moore⁡X|∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s
15 14 eleq2d ⊢X∈V→C∈ACS⁡X↔C∈c∈Moore⁡X|∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s
16 eleq2 ⊢c=C→s∈c↔s∈C
17 16 bibi1d ⊢c=C→s∈c↔⋃f𝒫s∩Fin⊆s↔s∈C↔⋃f𝒫s∩Fin⊆s
18 17 ralbidv ⊢c=C→∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s↔∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s
19 18 anbi2d ⊢c=C→f:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s↔f:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s
20 19 exbidv ⊢c=C→∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s↔∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s
21 20 elrab ⊢C∈c∈Moore⁡X|∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈c↔⋃f𝒫s∩Fin⊆s↔C∈Moore⁡X∧∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s
22 15 21 bitrdi ⊢X∈V→C∈ACS⁡X↔C∈Moore⁡X∧∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s
23 1 3 22 pm5.21nii ⊢C∈ACS⁡X↔C∈Moore⁡X∧∃ff:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔⋃f𝒫s∩Fin⊆s