Metamath Proof Explorer

Theorem mrcval

Description: Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015) (Proof shortened by Fan Zheng, 6-Jun-2016)

		Ref	Expression
	Hypothesis	mrcfval.f	$⊢ F = mrCls (C)$
	Assertion	mrcval	$⊢ (C \in Moore (X) \land U \subseteq X) \to F (U) = ⋂ \{s \in C \| U \subseteq s\}$

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$⊢ F = mrCls (C)$
2	1	mrcfval	$⊢ C \in Moore (X) \to F = (x \in 𝒫 X ⟼ ⋂ \{s \in C \| x \subseteq s\})$
3	2	adantr	$⊢ (C \in Moore (X) \land U \subseteq X) \to F = (x \in 𝒫 X ⟼ ⋂ \{s \in C \| x \subseteq s\})$
4		sseq1	$⊢ x = U \to (x \subseteq s \leftrightarrow U \subseteq s)$
5	4	rabbidv	$⊢ x = U \to \{s \in C \| x \subseteq s\} = \{s \in C \| U \subseteq s\}$
6	5	inteqd	$⊢ x = U \to ⋂ \{s \in C \| x \subseteq s\} = ⋂ \{s \in C \| U \subseteq s\}$
7	6	adantl	$⊢ ((C \in Moore (X) \land U \subseteq X) \land x = U) \to ⋂ \{s \in C \| x \subseteq s\} = ⋂ \{s \in C \| U \subseteq s\}$
8		mre1cl	$⊢ C \in Moore (X) \to X \in C$
9		elpw2g	$⊢ X \in C \to (U \in 𝒫 X \leftrightarrow U \subseteq X)$
10	8 9	syl	$⊢ C \in Moore (X) \to (U \in 𝒫 X \leftrightarrow U \subseteq X)$
11	10	biimpar	$⊢ (C \in Moore (X) \land U \subseteq X) \to U \in 𝒫 X$
12		sseq2	$⊢ s = X \to (U \subseteq s \leftrightarrow U \subseteq X)$
13	8	adantr	$⊢ (C \in Moore (X) \land U \subseteq X) \to X \in C$
14		simpr	$⊢ (C \in Moore (X) \land U \subseteq X) \to U \subseteq X$
15	12 13 14	elrabd	$⊢ (C \in Moore (X) \land U \subseteq X) \to X \in \{s \in C \| U \subseteq s\}$
16	15	ne0d	$⊢ (C \in Moore (X) \land U \subseteq X) \to \{s \in C \| U \subseteq s\} \neq \emptyset$
17		intex	$⊢ \{s \in C \| U \subseteq s\} \neq \emptyset \leftrightarrow ⋂ \{s \in C \| U \subseteq s\} \in V$
18	16 17	sylib	$⊢ (C \in Moore (X) \land U \subseteq X) \to ⋂ \{s \in C \| U \subseteq s\} \in V$
19	3 7 11 18	fvmptd	$⊢ (C \in Moore (X) \land U \subseteq X) \to F (U) = ⋂ \{s \in C \| U \subseteq s\}$