Theorem mrefg3

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

	Ref	Expression
Hypothesis	isnacs.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	mrefg3	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑆 ⊆ ( 𝐹 ‘ 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnacs.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2	1	mrefg2	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ) )
3	2	adantr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ) )
4		eqss	⊢ ( 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ ( 𝑆 ⊆ ( 𝐹 ‘ 𝑔 ) ∧ ( 𝐹 ‘ 𝑔 ) ⊆ 𝑆 ) )
5		simpll	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
6		inss1	⊢ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝒫 𝑆
7	6	sseli	⊢ ( 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) → 𝑔 ∈ 𝒫 𝑆 )
8	7	elpwid	⊢ ( 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) → 𝑔 ⊆ 𝑆 )
9	8	adantl	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝑔 ⊆ 𝑆 )
10		simplr	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝑆 ∈ 𝐶 )
11	1	mrcsscl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑆 ∧ 𝑆 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑔 ) ⊆ 𝑆 )
12	5 9 10 11	syl3anc	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → ( 𝐹 ‘ 𝑔 ) ⊆ 𝑆 )
13	12	biantrud	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → ( 𝑆 ⊆ ( 𝐹 ‘ 𝑔 ) ↔ ( 𝑆 ⊆ ( 𝐹 ‘ 𝑔 ) ∧ ( 𝐹 ‘ 𝑔 ) ⊆ 𝑆 ) ) )
14	4 13	bitr4id	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → ( 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ 𝑆 ⊆ ( 𝐹 ‘ 𝑔 ) ) )
15	14	rexbidva	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑆 ⊆ ( 𝐹 ‘ 𝑔 ) ) )
16	3 15	bitrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑆 ⊆ ( 𝐹 ‘ 𝑔 ) ) )