Metamath Proof Explorer

Theorem mrefg2

Description: Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypothesis isnacs.f ⊢F=mrCls⁡C
Assertion mrefg2 ⊢C∈Moore⁡X→∃g∈𝒫X∩FinS=F⁡g↔∃g∈𝒫S∩FinS=F⁡g

Proof

Step Hyp Ref Expression
1 isnacs.f ⊢F=mrCls⁡C
2 1 mrcssid ⊢C∈Moore⁡X∧g⊆X→g⊆F⁡g
3 simpr ⊢C∈Moore⁡X∧g⊆F⁡g→g⊆F⁡g
4 1 mrcssv ⊢C∈Moore⁡X→F⁡g⊆X
5 4 adantr ⊢C∈Moore⁡X∧g⊆F⁡g→F⁡g⊆X
6 3 5 sstrd ⊢C∈Moore⁡X∧g⊆F⁡g→g⊆X
7 2 6 impbida ⊢C∈Moore⁡X→g⊆X↔g⊆F⁡g
8 vex ⊢g∈V
9 8 elpw ⊢g∈𝒫X↔g⊆X
10 8 elpw ⊢g∈𝒫F⁡g↔g⊆F⁡g
11 7 9 10 3bitr4g ⊢C∈Moore⁡X→g∈𝒫X↔g∈𝒫F⁡g
12 11 anbi1d ⊢C∈Moore⁡X→g∈𝒫X∧g∈Fin↔g∈𝒫F⁡g∧g∈Fin
13 elin ⊢g∈𝒫X∩Fin↔g∈𝒫X∧g∈Fin
14 elin ⊢g∈𝒫F⁡g∩Fin↔g∈𝒫F⁡g∧g∈Fin
15 12 13 14 3bitr4g ⊢C∈Moore⁡X→g∈𝒫X∩Fin↔g∈𝒫F⁡g∩Fin
16 pweq ⊢S=F⁡g→𝒫S=𝒫F⁡g
17 16 ineq1d ⊢S=F⁡g→𝒫S∩Fin=𝒫F⁡g∩Fin
18 17 eleq2d ⊢S=F⁡g→g∈𝒫S∩Fin↔g∈𝒫F⁡g∩Fin
19 18 bibi2d ⊢S=F⁡g→g∈𝒫X∩Fin↔g∈𝒫S∩Fin↔g∈𝒫X∩Fin↔g∈𝒫F⁡g∩Fin
20 15 19 syl5ibrcom ⊢C∈Moore⁡X→S=F⁡g→g∈𝒫X∩Fin↔g∈𝒫S∩Fin
21 20 pm5.32rd ⊢C∈Moore⁡X→g∈𝒫X∩Fin∧S=F⁡g↔g∈𝒫S∩Fin∧S=F⁡g
22 21 rexbidv2 ⊢C∈Moore⁡X→∃g∈𝒫X∩FinS=F⁡g↔∃g∈𝒫S∩FinS=F⁡g