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 ∩ Fin S = F ⁡ g ↔ ∃ g ∈ 𝒫 S ∩ Fin S = 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 ∩ Fin S = F ⁡ g ↔ ∃ g ∈ 𝒫 S ∩ Fin S = F ⁡ g