Metamath Proof Explorer


Theorem mrefg3

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 mrefg3 C Moore X S C 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 mrefg2 C Moore X g 𝒫 X Fin S = F g g 𝒫 S Fin S = F g
3 2 adantr C Moore X S C g 𝒫 X Fin S = F g g 𝒫 S Fin S = F g
4 eqss S = F g S F g F g S
5 simpll C Moore X S C g 𝒫 S Fin C Moore X
6 inss1 𝒫 S Fin 𝒫 S
7 6 sseli g 𝒫 S Fin g 𝒫 S
8 7 elpwid g 𝒫 S Fin g S
9 8 adantl C Moore X S C g 𝒫 S Fin g S
10 simplr C Moore X S C g 𝒫 S Fin S C
11 1 mrcsscl C Moore X g S S C F g S
12 5 9 10 11 syl3anc C Moore X S C g 𝒫 S Fin F g S
13 12 biantrud C Moore X S C g 𝒫 S Fin S F g S F g F g S
14 4 13 bitr4id C Moore X S C g 𝒫 S Fin S = F g S F g
15 14 rexbidva C Moore X S C g 𝒫 S Fin S = F g g 𝒫 S Fin S F g
16 3 15 bitrd C Moore X S C g 𝒫 X Fin S = F g g 𝒫 S Fin S F g