submre

Description: The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015)

		Ref	Expression
	Assertion	submre	$⊢ (C \in Moore (X) \land A \in C) \to C \cap 𝒫 A \in Moore (A)$

Proof

Step	Hyp	Ref	Expression
1		inss2	$⊢ C \cap 𝒫 A \subseteq 𝒫 A$
2	1	a1i	$⊢ (C \in Moore (X) \land A \in C) \to C \cap 𝒫 A \subseteq 𝒫 A$
3		simpr	$⊢ (C \in Moore (X) \land A \in C) \to A \in C$
4		pwidg	$⊢ A \in C \to A \in 𝒫 A$
5	4	adantl	$⊢ (C \in Moore (X) \land A \in C) \to A \in 𝒫 A$
6	3 5	elind	$⊢ (C \in Moore (X) \land A \in C) \to A \in (C \cap 𝒫 A)$
7		simp1l	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to C \in Moore (X)$
8		inss1	$⊢ C \cap 𝒫 A \subseteq C$
9		sstr	$⊢ (x \subseteq C \cap 𝒫 A \land C \cap 𝒫 A \subseteq C) \to x \subseteq C$
10	8 9	mpan2	$⊢ x \subseteq C \cap 𝒫 A \to x \subseteq C$
11	10	3ad2ant2	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to x \subseteq C$
12		simp3	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to x \neq \emptyset$
13		mreintcl	$⊢ (C \in Moore (X) \land x \subseteq C \land x \neq \emptyset) \to ⋂ x \in C$
14	7 11 12 13	syl3anc	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to ⋂ x \in C$
15		sstr	$⊢ (x \subseteq C \cap 𝒫 A \land C \cap 𝒫 A \subseteq 𝒫 A) \to x \subseteq 𝒫 A$
16	1 15	mpan2	$⊢ x \subseteq C \cap 𝒫 A \to x \subseteq 𝒫 A$
17	16	3ad2ant2	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to x \subseteq 𝒫 A$
18		intssuni2	$⊢ (x \subseteq 𝒫 A \land x \neq \emptyset) \to ⋂ x \subseteq ⋃ 𝒫 A$
19	17 12 18	syl2anc	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to ⋂ x \subseteq ⋃ 𝒫 A$
20		unipw	$⊢ ⋃ 𝒫 A = A$
21	19 20	sseqtrdi	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to ⋂ x \subseteq A$
22		elpw2g	$⊢ A \in C \to (⋂ x \in 𝒫 A \leftrightarrow ⋂ x \subseteq A)$
23	22	adantl	$⊢ (C \in Moore (X) \land A \in C) \to (⋂ x \in 𝒫 A \leftrightarrow ⋂ x \subseteq A)$
24	23	3ad2ant1	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to (⋂ x \in 𝒫 A \leftrightarrow ⋂ x \subseteq A)$
25	21 24	mpbird	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to ⋂ x \in 𝒫 A$
26	14 25	elind	$⊢ ((C \in Moore (X) \land A \in C) \land x \subseteq C \cap 𝒫 A \land x \neq \emptyset) \to ⋂ x \in (C \cap 𝒫 A)$
27	2 6 26	ismred	$⊢ (C \in Moore (X) \land A \in C) \to C \cap 𝒫 A \in Moore (A)$

Metamath Proof Explorer

Theorem submre

Proof