mrcflem

Description: The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015)

		Ref	Expression
	Assertion	mrcflem	$⊢ C \in Moore (X) \to (x \in 𝒫 X ⟼ ⋂ \{s \in C \| x \subseteq s\}) : 𝒫 X ⟶ C$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (C \in Moore (X) \land x \in 𝒫 X) \to C \in Moore (X)$
2		ssrab2	$⊢ \{s \in C \| x \subseteq s\} \subseteq C$
3	2	a1i	$⊢ (C \in Moore (X) \land x \in 𝒫 X) \to \{s \in C \| x \subseteq s\} \subseteq C$
4		sseq2	$⊢ s = X \to (x \subseteq s \leftrightarrow x \subseteq X)$
5		mre1cl	$⊢ C \in Moore (X) \to X \in C$
6	5	adantr	$⊢ (C \in Moore (X) \land x \in 𝒫 X) \to X \in C$
7		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
8	7	adantl	$⊢ (C \in Moore (X) \land x \in 𝒫 X) \to x \subseteq X$
9	4 6 8	elrabd	$⊢ (C \in Moore (X) \land x \in 𝒫 X) \to X \in \{s \in C \| x \subseteq s\}$
10	9	ne0d	$⊢ (C \in Moore (X) \land x \in 𝒫 X) \to \{s \in C \| x \subseteq s\} \neq \emptyset$
11		mreintcl	$⊢ (C \in Moore (X) \land \{s \in C \| x \subseteq s\} \subseteq C \land \{s \in C \| x \subseteq s\} \neq \emptyset) \to ⋂ \{s \in C \| x \subseteq s\} \in C$
12	1 3 10 11	syl3anc	$⊢ (C \in Moore (X) \land x \in 𝒫 X) \to ⋂ \{s \in C \| x \subseteq s\} \in C$
13	12	fmpttd	$⊢ C \in Moore (X) \to (x \in 𝒫 X ⟼ ⋂ \{s \in C \| x \subseteq s\}) : 𝒫 X ⟶ C$

Metamath Proof Explorer