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 ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion mrefg2 ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ) )

Proof

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