ismred2

Description: Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Hypotheses	ismred2.ss	$⊢ φ \to C \subseteq 𝒫 X$
	ismred2.in	$⊢ (φ \land s \subseteq C) \to X \cap ⋂ s \in C$
Assertion	ismred2	$⊢ φ \to C \in Moore (X)$

Proof

Step	Hyp	Ref	Expression
1		ismred2.ss	$⊢ φ \to C \subseteq 𝒫 X$
2		ismred2.in	$⊢ (φ \land s \subseteq C) \to X \cap ⋂ s \in C$
3		eqid	$⊢ \emptyset = \emptyset$
4		rint0	$⊢ \emptyset = \emptyset \to X \cap ⋂ \emptyset = X$
5	3 4	ax-mp	$⊢ X \cap ⋂ \emptyset = X$
6		0ss	$⊢ \emptyset \subseteq C$
7		0ex	$⊢ \emptyset \in V$
8		sseq1	$⊢ s = \emptyset \to (s \subseteq C \leftrightarrow \emptyset \subseteq C)$
9	8	anbi2d	$⊢ s = \emptyset \to ((φ \land s \subseteq C) \leftrightarrow (φ \land \emptyset \subseteq C))$
10		inteq	$⊢ s = \emptyset \to ⋂ s = ⋂ \emptyset$
11	10	ineq2d	$⊢ s = \emptyset \to X \cap ⋂ s = X \cap ⋂ \emptyset$
12	11	eleq1d	$⊢ s = \emptyset \to (X \cap ⋂ s \in C \leftrightarrow X \cap ⋂ \emptyset \in C)$
13	9 12	imbi12d	$⊢ s = \emptyset \to (((φ \land s \subseteq C) \to X \cap ⋂ s \in C) \leftrightarrow ((φ \land \emptyset \subseteq C) \to X \cap ⋂ \emptyset \in C))$
14	7 13 2	vtocl	$⊢ (φ \land \emptyset \subseteq C) \to X \cap ⋂ \emptyset \in C$
15	6 14	mpan2	$⊢ φ \to X \cap ⋂ \emptyset \in C$
16	5 15	eqeltrrid	$⊢ φ \to X \in C$
17		simp2	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to s \subseteq C$
18	1	3ad2ant1	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to C \subseteq 𝒫 X$
19	17 18	sstrd	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to s \subseteq 𝒫 X$
20		simp3	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to s \neq \emptyset$
21		rintn0	$⊢ (s \subseteq 𝒫 X \land s \neq \emptyset) \to X \cap ⋂ s = ⋂ s$
22	19 20 21	syl2anc	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to X \cap ⋂ s = ⋂ s$
23	2	3adant3	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to X \cap ⋂ s \in C$
24	22 23	eqeltrrd	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to ⋂ s \in C$
25	1 16 24	ismred	$⊢ φ \to C \in Moore (X)$

Metamath Proof Explorer

Theorem ismred2

Proof