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 \in Moore (X) \land S \in C) \to (\exists g \in (𝒫 X \cap Fin) S = F (g) \leftrightarrow \exists g \in (𝒫 S \cap Fin) S \subseteq F (g))$

Proof

Step	Hyp	Ref	Expression
1		isnacs.f	$⊢ F = mrCls (C)$
2	1	mrefg2	$⊢ C \in Moore (X) \to (\exists g \in (𝒫 X \cap Fin) S = F (g) \leftrightarrow \exists g \in (𝒫 S \cap Fin) S = F (g))$
3	2	adantr	$⊢ (C \in Moore (X) \land S \in C) \to (\exists g \in (𝒫 X \cap Fin) S = F (g) \leftrightarrow \exists g \in (𝒫 S \cap Fin) S = F (g))$
4		eqss	$⊢ S = F (g) \leftrightarrow (S \subseteq F (g) \land F (g) \subseteq S)$
5		simpll	$⊢ ((C \in Moore (X) \land S \in C) \land g \in (𝒫 S \cap Fin)) \to C \in Moore (X)$
6		inss1	$⊢ 𝒫 S \cap Fin \subseteq 𝒫 S$
7	6	sseli	$⊢ g \in (𝒫 S \cap Fin) \to g \in 𝒫 S$
8	7	elpwid	$⊢ g \in (𝒫 S \cap Fin) \to g \subseteq S$
9	8	adantl	$⊢ ((C \in Moore (X) \land S \in C) \land g \in (𝒫 S \cap Fin)) \to g \subseteq S$
10		simplr	$⊢ ((C \in Moore (X) \land S \in C) \land g \in (𝒫 S \cap Fin)) \to S \in C$
11	1	mrcsscl	$⊢ (C \in Moore (X) \land g \subseteq S \land S \in C) \to F (g) \subseteq S$
12	5 9 10 11	syl3anc	$⊢ ((C \in Moore (X) \land S \in C) \land g \in (𝒫 S \cap Fin)) \to F (g) \subseteq S$
13	12	biantrud	$⊢ ((C \in Moore (X) \land S \in C) \land g \in (𝒫 S \cap Fin)) \to (S \subseteq F (g) \leftrightarrow (S \subseteq F (g) \land F (g) \subseteq S))$
14	4 13	bitr4id	$⊢ ((C \in Moore (X) \land S \in C) \land g \in (𝒫 S \cap Fin)) \to (S = F (g) \leftrightarrow S \subseteq F (g))$
15	14	rexbidva	$⊢ (C \in Moore (X) \land S \in C) \to (\exists g \in (𝒫 S \cap Fin) S = F (g) \leftrightarrow \exists g \in (𝒫 S \cap Fin) S \subseteq F (g))$
16	3 15	bitrd	$⊢ (C \in Moore (X) \land S \in C) \to (\exists g \in (𝒫 X \cap Fin) S = F (g) \leftrightarrow \exists g \in (𝒫 S \cap Fin) S \subseteq F (g))$